theorem pim2im {x y: nat} (p1 q1: wff x) (p2 q2: wff y):
$ A. x (p1 -> (P. y p2 -> q1 -> q2)) -> (P. x p1 -> q1) -> (P. y p2 -> q2) $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
eexb |
E. x p1 -> (P. y p2 -> q2) <-> A. x (p1 -> (P. y p2 -> q2)) |
| 2 |
|
impim |
(P. y p2 -> q1 -> q2) -> q1 -> (P. y p2 -> q2) |
| 3 |
2 |
imim2i |
(p1 -> (P. y p2 -> q1 -> q2)) -> p1 -> q1 -> (P. y p2 -> q2) |
| 4 |
3 |
a2d |
(p1 -> (P. y p2 -> q1 -> q2)) -> (p1 -> q1) -> p1 -> (P. y p2 -> q2) |
| 5 |
4 |
al2imi |
A. x (p1 -> (P. y p2 -> q1 -> q2)) -> A. x (p1 -> q1) -> A. x (p1 -> (P. y p2 -> q2)) |
| 6 |
1, 5 |
syl6ibr |
A. x (p1 -> (P. y p2 -> q1 -> q2)) -> A. x (p1 -> q1) -> E. x p1 -> (P. y p2 -> q2) |
| 7 |
6 |
com23 |
A. x (p1 -> (P. y p2 -> q1 -> q2)) -> E. x p1 -> A. x (p1 -> q1) -> (P. y p2 -> q2) |
| 8 |
7 |
impd |
A. x (p1 -> (P. y p2 -> q1 -> q2)) -> E. x p1 /\ A. x (p1 -> q1) -> (P. y p2 -> q2) |
| 9 |
8 |
conv pim |
A. x (p1 -> (P. y p2 -> q1 -> q2)) -> (P. x p1 -> q1) -> (P. y p2 -> q2) |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp,
itru),
axs_pred_calc
(ax_gen,
ax_4,
ax_5,
ax_6,
ax_7,
ax_10,
ax_12)