Step |
Hyp |
Ref |
Expression |
1 |
|
exancom |
⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) ) |
2 |
1
|
anbi1i |
⊢ ( ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ↔ ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ) |
3 |
2
|
anbi2i |
⊢ ( ( ∃* 𝑥 𝜓 ∧ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ) ↔ ( ∃* 𝑥 𝜓 ∧ ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ) ) |
4 |
|
3anass |
⊢ ( ( ∃* 𝑥 𝜓 ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ↔ ( ∃* 𝑥 𝜓 ∧ ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ) ) |
5 |
3 4
|
bitr4i |
⊢ ( ( ∃* 𝑥 𝜓 ∧ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ) ↔ ( ∃* 𝑥 𝜓 ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ) |
6 |
|
mopick2 |
⊢ ( ( ∃* 𝑥 𝜓 ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) → ∃ 𝑥 ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) ) |
7 |
5 6
|
sylbi |
⊢ ( ( ∃* 𝑥 𝜓 ∧ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ) → ∃ 𝑥 ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) ) |
8 |
|
3anass |
⊢ ( ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) ↔ ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ) ) ) |
9 |
8
|
exbii |
⊢ ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) ↔ ∃ 𝑥 ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ) ) ) |
10 |
|
exsimpr |
⊢ ( ∃ 𝑥 ( 𝜓 ∧ ( 𝜑 ∧ 𝜒 ) ) → ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ) |
11 |
9 10
|
sylbi |
⊢ ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ∧ 𝜒 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ) |
12 |
7 11
|
syl |
⊢ ( ( ∃* 𝑥 𝜓 ∧ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ) → ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ) |
13 |
|
impexp |
⊢ ( ( ( ∃* 𝑥 𝜓 ∧ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ) → ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ) ↔ ( ∃* 𝑥 𝜓 → ( ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) → ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ) ) ) |
14 |
12 13
|
mpbi |
⊢ ( ∃* 𝑥 𝜓 → ( ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) → ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ) ) |