Metamath Proof Explorer


Theorem exsimpr

Description: Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion exsimpr xφψxψ

Proof

Step Hyp Ref Expression
1 simpr φψψ
2 1 eximi xφψxψ