Metamath Proof Explorer


Theorem bnj1351

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

Ref Expression
Hypothesis bnj1351.1
|- ( ph -> A. x ph )
Assertion bnj1351
|- ( ( ph /\ ps ) -> A. x ( ph /\ ps ) )

Proof

Step Hyp Ref Expression
1 bnj1351.1
 |-  ( ph -> A. x ph )
2 ax-5
 |-  ( ps -> A. x ps )
3 1 2 hban
 |-  ( ( ph /\ ps ) -> A. x ( ph /\ ps ) )