Theorem con1b | index | src |

theorem con1b (a b: wff): $ (~a <-> b) -> (~b <-> a) $;
StepHypRefExpression
1 bi1
(~a <-> b) -> ~a -> b
2 1 con1d
(~a <-> b) -> ~b -> a
3 bi2
(~a <-> b) -> b -> ~a
4 3 con2d
(~a <-> b) -> a -> ~b
5 2, 4 ibid
(~a <-> b) -> (~b <-> a)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)