Theorem bibin1 | index | src |

theorem bibin1 (a b: wff): $ ~a -> (a <-> b <-> ~b) $;
StepHypRefExpression
1 noteq
(a <-> b) -> (~a <-> ~b)
2 1 bi1d
(a <-> b) -> ~a -> ~b
3 2 com12
~a -> (a <-> b) -> ~b
4 binth
~a -> ~b -> (a <-> b)
5 3, 4 ibid
~a -> (a <-> b <-> ~b)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)