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

Metamath Proof Explorer

Theorem exancom

Description: Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993)

Ref Expression
Assertion exancom ⊢ ∃ x φ ∧ ψ ↔ ∃ x ψ ∧ φ

Proof

Step Hyp Ref Expression
1 ancom ⊢ φ ∧ ψ ↔ ψ ∧ φ
2 1 exbii ⊢ ∃ x φ ∧ ψ ↔ ∃ x ψ ∧ φ