Theorem cases | index | src |

theorem cases (a b: wff): $ a -> b $ > $ ~a -> b $ > $ b $;
StepHypRefExpression
1 contra
(~b -> b) -> b
2 hyp h1
a -> b
3 con1
(~a -> b) -> ~b -> a
4 hyp h2
~a -> b
5 3, 4 ax_mp
~b -> a
6 2, 5 syl
~b -> b
7 1, 6 ax_mp
b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)