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 φ ψ


Step Hyp Ref Expression
1 abai φ ψ φ φ ψ
2 1 rbaibr φ ψ φ φ ψ
3 2 alexbii x φ ψ x φ x φ ψ