theorem ifpnot (a b p: wff): $ ifp (~p) a b <-> ifp p b a $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
bitr4 |
(ifp (~p) a b <-> ~~p /\ b \/ ~p /\ a) -> (ifp p b a <-> ~~p /\ b \/ ~p /\ a) -> (ifp (~p) a b <-> ifp p b a) |
| 2 |
|
orcomb |
~p /\ a \/ ~~p /\ b <-> ~~p /\ b \/ ~p /\ a |
| 3 |
2 |
conv ifp |
ifp (~p) a b <-> ~~p /\ b \/ ~p /\ a |
| 4 |
1, 3 |
ax_mp |
(ifp p b a <-> ~~p /\ b \/ ~p /\ a) -> (ifp (~p) a b <-> ifp p b a) |
| 5 |
|
oreq1 |
(p /\ b <-> ~~p /\ b) -> (p /\ b \/ ~p /\ a <-> ~~p /\ b \/ ~p /\ a) |
| 6 |
5 |
conv ifp |
(p /\ b <-> ~~p /\ b) -> (ifp p b a <-> ~~p /\ b \/ ~p /\ a) |
| 7 |
|
notnot |
p <-> ~~p |
| 8 |
7 |
aneq1i |
p /\ b <-> ~~p /\ b |
| 9 |
6, 8 |
ax_mp |
ifp p b a <-> ~~p /\ b \/ ~p /\ a |
| 10 |
4, 9 |
ax_mp |
ifp (~p) a b <-> ifp p b a |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp)