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

Metamath Proof Explorer

Theorem exintrbi

Description: Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006)

Ref Expression
Assertion exintrbi ⊢ ∀ x φ → ψ → ∃ x φ ↔ ∃ x φ ∧ ψ

Proof

Step Hyp Ref Expression
1 abai ⊢ φ ∧ ψ ↔ φ ∧ φ → ψ
2 1 rbaibr ⊢ φ → ψ → φ ↔ φ ∧ ψ
3 2 alexbii ⊢ ∀ x φ → ψ → ∃ x φ ↔ ∃ x φ ∧ ψ