theorem pimeq2a {x: nat} (p q1 q2: wff x):
$ A. x (p -> (q1 <-> q2)) -> ((P. x p -> q1) <-> (P. x p -> q2)) $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
aleq |
A. x (p -> q1 <-> p -> q2) -> (A. x (p -> q1) <-> A. x (p -> q2)) |
| 2 |
|
imeq2a |
(p -> (q1 <-> q2)) -> (p -> q1 <-> p -> q2) |
| 3 |
2 |
alimi |
A. x (p -> (q1 <-> q2)) -> A. x (p -> q1 <-> p -> q2) |
| 4 |
1, 3 |
syl |
A. x (p -> (q1 <-> q2)) -> (A. x (p -> q1) <-> A. x (p -> q2)) |
| 5 |
4 |
aneq2d |
A. x (p -> (q1 <-> q2)) -> (E. x p /\ A. x (p -> q1) <-> E. x p /\ A. x (p -> q2)) |
| 6 |
5 |
conv pim |
A. x (p -> (q1 <-> q2)) -> ((P. x p -> q1) <-> (P. x p -> q2)) |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp),
axs_pred_calc
(ax_gen,
ax_4)