Metamath Proof Explorer


Theorem bnj596

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj596.1
|- ( ph -> A. x ph )
bnj596.2
|- ( ph -> E. x ps )
Assertion bnj596
|- ( ph -> E. x ( ph /\ ps ) )

Proof

Step Hyp Ref Expression
1 bnj596.1
 |-  ( ph -> A. x ph )
2 bnj596.2
 |-  ( ph -> E. x ps )
3 2 ancli
 |-  ( ph -> ( ph /\ E. x ps ) )
4 1 nf5i
 |-  F/ x ph
5 4 19.42
 |-  ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )
6 3 5 sylibr
 |-  ( ph -> E. x ( ph /\ ps ) )