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