Proof of Theorem moantr
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | exancom 1861 | . . . . . . 7
⊢
(∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) | 
| 2 | 1 | anbi1i 624 | . . . . . 6
⊢
((∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒)) ↔ (∃𝑥(𝜓 ∧ 𝜑) ∧ ∃𝑥(𝜓 ∧ 𝜒))) | 
| 3 | 2 | anbi2i 623 | . . . . 5
⊢
((∃*𝑥𝜓 ∧ (∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒))) ↔ (∃*𝑥𝜓 ∧ (∃𝑥(𝜓 ∧ 𝜑) ∧ ∃𝑥(𝜓 ∧ 𝜒)))) | 
| 4 |  | 3anass 1095 | . . . . 5
⊢
((∃*𝑥𝜓 ∧ ∃𝑥(𝜓 ∧ 𝜑) ∧ ∃𝑥(𝜓 ∧ 𝜒)) ↔ (∃*𝑥𝜓 ∧ (∃𝑥(𝜓 ∧ 𝜑) ∧ ∃𝑥(𝜓 ∧ 𝜒)))) | 
| 5 | 3, 4 | bitr4i 278 | . . . 4
⊢
((∃*𝑥𝜓 ∧ (∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒))) ↔ (∃*𝑥𝜓 ∧ ∃𝑥(𝜓 ∧ 𝜑) ∧ ∃𝑥(𝜓 ∧ 𝜒))) | 
| 6 |  | mopick2 2637 | . . . 4
⊢
((∃*𝑥𝜓 ∧ ∃𝑥(𝜓 ∧ 𝜑) ∧ ∃𝑥(𝜓 ∧ 𝜒)) → ∃𝑥(𝜓 ∧ 𝜑 ∧ 𝜒)) | 
| 7 | 5, 6 | sylbi 217 | . . 3
⊢
((∃*𝑥𝜓 ∧ (∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒))) → ∃𝑥(𝜓 ∧ 𝜑 ∧ 𝜒)) | 
| 8 |  | 3anass 1095 | . . . . 5
⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | 
| 9 | 8 | exbii 1848 | . . . 4
⊢
(∃𝑥(𝜓 ∧ 𝜑 ∧ 𝜒) ↔ ∃𝑥(𝜓 ∧ (𝜑 ∧ 𝜒))) | 
| 10 |  | exsimpr 1869 | . . . 4
⊢
(∃𝑥(𝜓 ∧ (𝜑 ∧ 𝜒)) → ∃𝑥(𝜑 ∧ 𝜒)) | 
| 11 | 9, 10 | sylbi 217 | . . 3
⊢
(∃𝑥(𝜓 ∧ 𝜑 ∧ 𝜒) → ∃𝑥(𝜑 ∧ 𝜒)) | 
| 12 | 7, 11 | syl 17 | . 2
⊢
((∃*𝑥𝜓 ∧ (∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒))) → ∃𝑥(𝜑 ∧ 𝜒)) | 
| 13 |  | impexp 450 | . 2
⊢
(((∃*𝑥𝜓 ∧ (∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒))) → ∃𝑥(𝜑 ∧ 𝜒)) ↔ (∃*𝑥𝜓 → ((∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒)) → ∃𝑥(𝜑 ∧ 𝜒)))) | 
| 14 | 12, 13 | mpbi 230 | 1
⊢
(∃*𝑥𝜓 → ((∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒)) → ∃𝑥(𝜑 ∧ 𝜒))) |