theorem pimeq1 {x: nat} (p1 p2 q: wff x):
$ A. x (p1 <-> p2) -> ((P. x p1 -> q) <-> (P. x p2 -> q)) $;
Step | Hyp | Ref | Expression |
1 |
|
exeq |
A. x (p1 <-> p2) -> (E. x p1 <-> E. x p2) |
2 |
|
aleq |
A. x (p1 -> q <-> p2 -> q) -> (A. x (p1 -> q) <-> A. x (p2 -> q)) |
3 |
|
id |
(p1 <-> p2) -> (p1 <-> p2) |
4 |
3 |
imeq1d |
(p1 <-> p2) -> (p1 -> q <-> p2 -> q) |
5 |
4 |
alimi |
A. x (p1 <-> p2) -> A. x (p1 -> q <-> p2 -> q) |
6 |
2, 5 |
syl |
A. x (p1 <-> p2) -> (A. x (p1 -> q) <-> A. x (p2 -> q)) |
7 |
1, 6 |
aneqd |
A. x (p1 <-> p2) -> (E. x p1 /\ A. x (p1 -> q) <-> E. x p2 /\ A. x (p2 -> q)) |
8 |
7 |
conv pim |
A. x (p1 <-> p2) -> ((P. x p1 -> q) <-> (P. x p2 -> q)) |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp),
axs_pred_calc
(ax_gen,
ax_4)