Originally Posted by

**emakarov** I agree.

Talking about (A&B) v (A→C) is misleading because you are actually proving ~B→(A→C), or A -> ~B -> C, which is almost the same thing. This is confirmed by the fact that you start the proof (in post #6) by assuming A and also by explicitly writing the fact you are proving: "given ax = 0, you can either assume a ≠ 0, and then prove x = 0." There are three cases when one assumes A in a proof: (1) when the claim has the form A -> ...; (2) when one uses the law of excluded middle (LEM) for A; and (3) when one proves a lemma of the form A -> ... Case (1) agrees with the fact that you are proving A -> ~B -> C; (2) is not the case here and (3) is more complicated than this problem is worth, especially when you are trying to explain it to somebody.

I am not arguing that A -> B \/ C is not equivalent to (A&B) v (A→C). I am just doubting that "mathematicians, when presented with a statement like: A → (B v C) like to prove instead: (A & B) v (A → C)." If you really started proving (A & B) v (A → C), you would start the proof either by LEM or by choosing one of the disjunct to prove. Instead, it is easier and more natural to prove A -> ~B -> C, which is also what you did.