theorem ifpeqd (_G _p1 _p2 _a1 _a2 _b1 _b2: wff):
$ _G -> (_p1 <-> _p2) $ >
$ _G -> (_a1 <-> _a2) $ >
$ _G -> (_b1 <-> _b2) $ >
$ _G -> (ifp _p1 _a1 _b1 <-> ifp _p2 _a2 _b2) $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
hyp _ph |
_G -> (_p1 <-> _p2) |
| 2 |
|
hyp _ah |
_G -> (_a1 <-> _a2) |
| 3 |
1, 2 |
aneqd |
_G -> (_p1 /\ _a1 <-> _p2 /\ _a2) |
| 4 |
1 |
noteqd |
_G -> (~_p1 <-> ~_p2) |
| 5 |
|
hyp _bh |
_G -> (_b1 <-> _b2) |
| 6 |
4, 5 |
aneqd |
_G -> (~_p1 /\ _b1 <-> ~_p2 /\ _b2) |
| 7 |
3, 6 |
oreqd |
_G -> (_p1 /\ _a1 \/ ~_p1 /\ _b1 <-> _p2 /\ _a2 \/ ~_p2 /\ _b2) |
| 8 |
7 |
conv ifp |
_G -> (ifp _p1 _a1 _b1 <-> ifp _p2 _a2 _b2) |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp)