Step |
Hyp |
Ref |
Expression |
1 |
|
ax5e |
⊢ ( ∃ 𝑥 𝜓 → 𝜓 ) |
2 |
1
|
ax-gen |
⊢ ∀ 𝑦 ( ∃ 𝑥 𝜓 → 𝜓 ) |
3 |
|
ax-5 |
⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) |
4 |
|
bj-cbvalimt |
⊢ ( ∀ 𝑦 ∃ 𝑥 𝜒 → ( ∀ 𝑦 ∀ 𝑥 ( 𝜒 → ( 𝜑 → 𝜓 ) ) → ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) → ( ∀ 𝑦 ( ∃ 𝑥 𝜓 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) ) ) ) |
5 |
4
|
com3l |
⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝜒 → ( 𝜑 → 𝜓 ) ) → ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) → ( ∀ 𝑦 ∃ 𝑥 𝜒 → ( ∀ 𝑦 ( ∃ 𝑥 𝜓 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) ) ) ) |
6 |
5
|
com14 |
⊢ ( ∀ 𝑦 ( ∃ 𝑥 𝜓 → 𝜓 ) → ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) → ( ∀ 𝑦 ∃ 𝑥 𝜒 → ( ∀ 𝑦 ∀ 𝑥 ( 𝜒 → ( 𝜑 → 𝜓 ) ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) ) ) ) |
7 |
2 3 6
|
mp2 |
⊢ ( ∀ 𝑦 ∃ 𝑥 𝜒 → ( ∀ 𝑦 ∀ 𝑥 ( 𝜒 → ( 𝜑 → 𝜓 ) ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) ) |