This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem moantr

Description: Sufficient condition for transitivity of conjunctions inside existential quantifiers. (Contributed by Peter Mazsa, 2-Oct-2018)

Ref Expression
Assertion moantr ⊢ ∃* x ψ → ∃ x φ ∧ ψ ∧ ∃ x ψ ∧ χ → ∃ x φ ∧ χ

Proof

Step Hyp Ref Expression
1 exancom ⊢ ∃ x φ ∧ ψ ↔ ∃ x ψ ∧ φ
2 1 anbi1i ⊢ ∃ x φ ∧ ψ ∧ ∃ x ψ ∧ χ ↔ ∃ x ψ ∧ φ ∧ ∃ x ψ ∧ χ
3 2 anbi2i ⊢ ∃* x ψ ∧ ∃ x φ ∧ ψ ∧ ∃ x ψ ∧ χ ↔ ∃* x ψ ∧ ∃ x ψ ∧ φ ∧ ∃ x ψ ∧ χ
4 3anass ⊢ ∃* x ψ ∧ ∃ x ψ ∧ φ ∧ ∃ x ψ ∧ χ ↔ ∃* x ψ ∧ ∃ x ψ ∧ φ ∧ ∃ x ψ ∧ χ
5 3 4 bitr4i ⊢ ∃* x ψ ∧ ∃ x φ ∧ ψ ∧ ∃ x ψ ∧ χ ↔ ∃* x ψ ∧ ∃ x ψ ∧ φ ∧ ∃ x ψ ∧ χ
6 mopick2 ⊢ ∃* x ψ ∧ ∃ x ψ ∧ φ ∧ ∃ x ψ ∧ χ → ∃ x ψ ∧ φ ∧ χ
7 5 6 sylbi ⊢ ∃* x ψ ∧ ∃ x φ ∧ ψ ∧ ∃ x ψ ∧ χ → ∃ x ψ ∧ φ ∧ χ
8 3anass ⊢ ψ ∧ φ ∧ χ ↔ ψ ∧ φ ∧ χ
9 8 exbii ⊢ ∃ x ψ ∧ φ ∧ χ ↔ ∃ x ψ ∧ φ ∧ χ
10 exsimpr ⊢ ∃ x ψ ∧ φ ∧ χ → ∃ x φ ∧ χ
11 9 10 sylbi ⊢ ∃ x ψ ∧ φ ∧ χ → ∃ x φ ∧ χ
12 7 11 syl ⊢ ∃* x ψ ∧ ∃ x φ ∧ ψ ∧ ∃ x ψ ∧ χ → ∃ x φ ∧ χ
13 impexp ⊢ ∃* x ψ ∧ ∃ x φ ∧ ψ ∧ ∃ x ψ ∧ χ → ∃ x φ ∧ χ ↔ ∃* x ψ → ∃ x φ ∧ ψ ∧ ∃ x ψ ∧ χ → ∃ x φ ∧ χ
14 12 13 mpbi ⊢ ∃* x ψ → ∃ x φ ∧ ψ ∧ ∃ x ψ ∧ χ → ∃ x φ ∧ χ