Step |
Hyp |
Ref |
Expression |
1 |
|
frege59c.a |
⊢ 𝐴 ∈ 𝐵 |
2 |
1
|
frege58c |
⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) |
3 |
|
sbcim1 |
⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) |
4 |
|
sbcim1 |
⊢ ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) |
5 |
3 4
|
syl6 |
⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) |
6 |
2 5
|
syl |
⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) |
7 |
|
frege12 |
⊢ ( ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) → ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜓 → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) ) |
8 |
6 7
|
ax-mp |
⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜓 → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) |