Theorem notor | index | src |

theorem notor (a b: wff): $ ~(a \/ b) <-> ~a /\ ~b $;
StepHypRefExpression
1 con1b
(~(~a /\ ~b) <-> a \/ b) -> (~(a \/ b) <-> ~a /\ ~b)
2 bitr4
(~(~a /\ ~b) <-> ~~a \/ ~~b) -> (a \/ b <-> ~~a \/ ~~b) -> (~(~a /\ ~b) <-> a \/ b)
3 notan
~(~a /\ ~b) <-> ~~a \/ ~~b
4 2, 3 ax_mp
(a \/ b <-> ~~a \/ ~~b) -> (~(~a /\ ~b) <-> a \/ b)
5 notnot
a <-> ~~a
6 notnot
b <-> ~~b
7 5, 6 oreqi
a \/ b <-> ~~a \/ ~~b
8 4, 7 ax_mp
~(~a /\ ~b) <-> a \/ b
9 1, 8 ax_mp
~(a \/ b) <-> ~a /\ ~b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)