theorem ifpan1 (a b c p: wff): $ ifp p a b /\ c <-> ifp p (a /\ c) (b /\ c) $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
bitr |
(ifp p a b /\ c <-> p /\ a /\ c \/ ~p /\ b /\ c) -> (p /\ a /\ c \/ ~p /\ b /\ c <-> ifp p (a /\ c) (b /\ c)) -> (ifp p a b /\ c <-> ifp p (a /\ c) (b /\ c)) |
| 2 |
|
andir |
(p /\ a \/ ~p /\ b) /\ c <-> p /\ a /\ c \/ ~p /\ b /\ c |
| 3 |
2 |
conv ifp |
ifp p a b /\ c <-> p /\ a /\ c \/ ~p /\ b /\ c |
| 4 |
1, 3 |
ax_mp |
(p /\ a /\ c \/ ~p /\ b /\ c <-> ifp p (a /\ c) (b /\ c)) -> (ifp p a b /\ c <-> ifp p (a /\ c) (b /\ c)) |
| 5 |
|
oreq |
(p /\ a /\ c <-> p /\ (a /\ c)) -> (~p /\ b /\ c <-> ~p /\ (b /\ c)) -> (p /\ a /\ c \/ ~p /\ b /\ c <-> p /\ (a /\ c) \/ ~p /\ (b /\ c)) |
| 6 |
5 |
conv ifp |
(p /\ a /\ c <-> p /\ (a /\ c)) -> (~p /\ b /\ c <-> ~p /\ (b /\ c)) -> (p /\ a /\ c \/ ~p /\ b /\ c <-> ifp p (a /\ c) (b /\ c)) |
| 7 |
|
anass |
p /\ a /\ c <-> p /\ (a /\ c) |
| 8 |
6, 7 |
ax_mp |
(~p /\ b /\ c <-> ~p /\ (b /\ c)) -> (p /\ a /\ c \/ ~p /\ b /\ c <-> ifp p (a /\ c) (b /\ c)) |
| 9 |
|
anass |
~p /\ b /\ c <-> ~p /\ (b /\ c) |
| 10 |
8, 9 |
ax_mp |
p /\ a /\ c \/ ~p /\ b /\ c <-> ifp p (a /\ c) (b /\ c) |
| 11 |
4, 10 |
ax_mp |
ifp p a b /\ c <-> ifp p (a /\ c) (b /\ c) |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp)