A formal argument in logic in which it is stated that

1. and (where means "implies"), and

2. Either not- or not- is true, from which two statements it follows that either not- or not- is true.