Step |
Hyp |
Ref |
Expression |
1 |
|
idn1 |
⊢ ( 𝐴 ∈ 𝐵 ▶ 𝐴 ∈ 𝐵 ) |
2 |
|
idn2 |
⊢ ( 𝐴 ∈ 𝐵 , [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ▶ [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) |
3 |
|
sbcimg |
⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) ) |
4 |
3
|
biimpd |
⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) ) |
5 |
1 2 4
|
e12 |
⊢ ( 𝐴 ∈ 𝐵 , [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ▶ ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) |
6 |
|
sbcimg |
⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) |
7 |
1 6
|
e1a |
⊢ ( 𝐴 ∈ 𝐵 ▶ ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) |
8 |
|
imbi2 |
⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) ) |
9 |
8
|
biimpcd |
⊢ ( ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) ) |
10 |
5 7 9
|
e21 |
⊢ ( 𝐴 ∈ 𝐵 , [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ▶ ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) |
11 |
10
|
in2 |
⊢ ( 𝐴 ∈ 𝐵 ▶ ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) ) |
12 |
|
idn2 |
⊢ ( 𝐴 ∈ 𝐵 , ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ▶ ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) |
13 |
|
biimpr |
⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) |
14 |
13
|
imim2d |
⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) ) |
15 |
7 12 14
|
e12 |
⊢ ( 𝐴 ∈ 𝐵 , ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ▶ ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) |
16 |
1 3
|
e1a |
⊢ ( 𝐴 ∈ 𝐵 ▶ ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) ) |
17 |
|
biimpr |
⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) → ( ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) → [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) ) |
18 |
17
|
com12 |
⊢ ( ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) → [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) ) |
19 |
15 16 18
|
e21 |
⊢ ( 𝐴 ∈ 𝐵 , ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ▶ [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) |
20 |
19
|
in2 |
⊢ ( 𝐴 ∈ 𝐵 ▶ ( ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) ) |
21 |
|
impbi |
⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) → ( ( ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) ) ) |
22 |
11 20 21
|
e11 |
⊢ ( 𝐴 ∈ 𝐵 ▶ ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) ) |
23 |
22
|
in1 |
⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) ) |