theorem nbioran (a b: wff): $ ~(a <-> b) <-> (a \/ b) /\ ~(a /\ b) $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
con1bb |
~((a \/ b) /\ ~(a /\ b)) <-> (a <-> b) <-> (~(a <-> b) <-> (a \/ b) /\ ~(a /\ b)) |
| 2 |
|
bitr2 |
(a <-> b <-> a \/ b -> a /\ b) -> (a \/ b -> a /\ b <-> ~((a \/ b) /\ ~(a /\ b))) -> (~((a \/ b) /\ ~(a /\ b)) <-> (a <-> b)) |
| 3 |
|
oriman |
a <-> b <-> a \/ b -> a /\ b |
| 4 |
2, 3 |
ax_mp |
(a \/ b -> a /\ b <-> ~((a \/ b) /\ ~(a /\ b))) -> (~((a \/ b) /\ ~(a /\ b)) <-> (a <-> b)) |
| 5 |
|
iman |
a \/ b -> a /\ b <-> ~((a \/ b) /\ ~(a /\ b)) |
| 6 |
4, 5 |
ax_mp |
~((a \/ b) /\ ~(a /\ b)) <-> (a <-> b) |
| 7 |
1, 6 |
mpbi |
~(a <-> b) <-> (a \/ b) /\ ~(a /\ b) |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp)