Theorem con2bi | index | src |

theorem con2bi (a b: wff): $ a -> ~b <-> b -> ~a $;
StepHypRefExpression
1 con2
(a -> ~b) -> b -> ~a
2 con2
(b -> ~a) -> a -> ~b
3 1, 2 ibii
a -> ~b <-> b -> ~a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)