theorem ifpor (a b c d p: wff):
$ ifp p (a \/ b) (c \/ d) <-> ifp p a c \/ ifp p b d $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
ifppos |
p -> (ifp p (a \/ b) (c \/ d) <-> a \/ b) |
| 2 |
|
ifppos |
p -> (ifp p a c <-> a) |
| 3 |
|
ifppos |
p -> (ifp p b d <-> b) |
| 4 |
2, 3 |
oreqd |
p -> (ifp p a c \/ ifp p b d <-> a \/ b) |
| 5 |
1, 4 |
bitr4d |
p -> (ifp p (a \/ b) (c \/ d) <-> ifp p a c \/ ifp p b d) |
| 6 |
|
ifpneg |
~p -> (ifp p (a \/ b) (c \/ d) <-> c \/ d) |
| 7 |
|
ifpneg |
~p -> (ifp p a c <-> c) |
| 8 |
|
ifpneg |
~p -> (ifp p b d <-> d) |
| 9 |
7, 8 |
oreqd |
~p -> (ifp p a c \/ ifp p b d <-> c \/ d) |
| 10 |
6, 9 |
bitr4d |
~p -> (ifp p (a \/ b) (c \/ d) <-> ifp p a c \/ ifp p b d) |
| 11 |
5, 10 |
cases |
ifp p (a \/ b) (c \/ d) <-> ifp p a c \/ ifp p b d |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp)