Theorem con3 | index | src |

theorem con3 (a b: wff): $ (a -> b) -> ~b -> ~a $;
StepHypRefExpression
1 con2
(a -> ~~b) -> ~b -> ~a
2 notnot1
b -> ~~b
3 2 imim2i
(a -> b) -> a -> ~~b
4 1, 3 syl
(a -> b) -> ~b -> ~a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)