Step |
Hyp |
Ref |
Expression |
1 |
|
sbcimg |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) ) |
2 |
1
|
biimpd |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) ) |
3 |
|
sbcimg |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) |
4 |
|
imbi2 |
⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) ) |
5 |
4
|
biimpcd |
⊢ ( ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) ) |
6 |
2 3 5
|
syl6ci |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) ) |
7 |
|
idd |
⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) ) |
8 |
|
biimpr |
⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) |
9 |
3 7 8
|
ee13 |
⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) ) |
10 |
9 1
|
sylibrd |
⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) ) |
11 |
6 10
|
impbid |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) ) |