Step |
Hyp |
Ref |
Expression |
1 |
|
nfmo1 |
⊢ Ⅎ 𝑥 ∃* 𝑥 𝜑 |
2 |
|
nfe1 |
⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) |
3 |
1 2
|
nfan |
⊢ Ⅎ 𝑥 ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) |
4 |
|
mopick |
⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜑 → 𝜓 ) ) |
5 |
4
|
ancld |
⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜑 → ( 𝜑 ∧ 𝜓 ) ) ) |
6 |
5
|
anim1d |
⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ) ) |
7 |
|
df-3an |
⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ) |
8 |
6 7
|
syl6ibr |
⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( ( 𝜑 ∧ 𝜒 ) → ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ) ) |
9 |
3 8
|
eximd |
⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ) ) |
10 |
9
|
3impia |
⊢ ( ( ∃* 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ) |