theorem expim {x y: nat} (p: wff x) (q: wff x y):
$ E. y (P. x p -> q) -> (P. x p -> E. y q) $;
Step | Hyp | Ref | Expression |
1 |
|
anl |
E. x p /\ A. x (p -> q) -> E. x p |
2 |
1 |
conv pim |
(P. x p -> q) -> E. x p |
3 |
2 |
eximi |
E. y (P. x p -> q) -> E. y E. x p |
4 |
|
excom |
E. y E. x p -> E. x E. y p |
5 |
|
id |
p -> p |
6 |
5 |
eex |
E. y p -> p |
7 |
6 |
eximi |
E. x E. y p -> E. x p |
8 |
4, 7 |
rsyl |
E. y E. x p -> E. x p |
9 |
3, 8 |
rsyl |
E. y (P. x p -> q) -> E. x p |
10 |
|
exral |
E. y A. x (p -> q) -> A. x (p -> E. y q) |
11 |
|
anr |
E. x p /\ A. x (p -> q) -> A. x (p -> q) |
12 |
11 |
conv pim |
(P. x p -> q) -> A. x (p -> q) |
13 |
12 |
eximi |
E. y (P. x p -> q) -> E. y A. x (p -> q) |
14 |
10, 13 |
syl |
E. y (P. x p -> q) -> A. x (p -> E. y q) |
15 |
9, 14 |
iand |
E. y (P. x p -> q) -> E. x p /\ A. x (p -> E. y q) |
16 |
15 |
conv pim |
E. y (P. x p -> q) -> (P. x p -> E. y q) |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp),
axs_pred_calc
(ax_gen,
ax_4,
ax_5,
ax_6,
ax_7,
ax_10,
ax_11,
ax_12)