Theorem binth | index | src |

theorem binth (a b: wff): $ ~a -> ~b -> (a <-> b) $;
StepHypRefExpression
1 anl
~a /\ ~b -> ~a
2 anr
~a /\ ~b -> ~b
3 1, 2 binthd
~a /\ ~b -> (a <-> b)
4 3 exp
~a -> ~b -> (a <-> b)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)