theorem cbvpimh {x y: nat} (p1 p2 q1 q2: wff x y):
$ F/ y p1 $ >
$ F/ y q1 $ >
$ F/ x p2 $ >
$ F/ x q2 $ >
$ x = y -> (p1 <-> p2) $ >
$ x = y -> (q1 <-> q2) $ >
$ (P. x p1 -> q1) <-> (P. y p2 -> q2) $;
Step | Hyp | Ref | Expression |
1 |
|
aneq |
(E. x p1 <-> E. y p2) -> (A. x (p1 -> q1) <-> A. y (p2 -> q2)) -> (E. x p1 /\ A. x (p1 -> q1) <-> E. y p2 /\ A. y (p2 -> q2)) |
2 |
1 |
conv pim |
(E. x p1 <-> E. y p2) -> (A. x (p1 -> q1) <-> A. y (p2 -> q2)) -> ((P. x p1 -> q1) <-> (P. y p2 -> q2)) |
3 |
|
hyp h1 |
F/ y p1 |
4 |
|
hyp h3 |
F/ x p2 |
5 |
|
hyp e1 |
x = y -> (p1 <-> p2) |
6 |
3, 4, 5 |
cbvexh |
E. x p1 <-> E. y p2 |
7 |
2, 6 |
ax_mp |
(A. x (p1 -> q1) <-> A. y (p2 -> q2)) -> ((P. x p1 -> q1) <-> (P. y p2 -> q2)) |
8 |
|
hyp h2 |
F/ y q1 |
9 |
3, 8 |
nfim |
F/ y p1 -> q1 |
10 |
|
hyp h4 |
F/ x q2 |
11 |
4, 10 |
nfim |
F/ x p2 -> q2 |
12 |
|
hyp e2 |
x = y -> (q1 <-> q2) |
13 |
5, 12 |
imeqd |
x = y -> (p1 -> q1 <-> p2 -> q2) |
14 |
9, 11, 13 |
cbvalh |
A. x (p1 -> q1) <-> A. y (p2 -> q2) |
15 |
7, 14 |
ax_mp |
(P. x p1 -> q1) <-> (P. y p2 -> q2) |
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)