Metamath Proof Explorer


Theorem bj-genl

Description: Generalization rule on the left conjunct. See 19.27 . (Contributed by BJ, 7-Jul-2021)

Ref Expression
Hypothesis bj-genr.1
|- ( ph /\ ps )
Assertion bj-genl
|- ( A. x ph /\ ps )

Proof

Step Hyp Ref Expression
1 bj-genr.1
 |-  ( ph /\ ps )
2 1 simpli
 |-  ph
3 2 ax-gen
 |-  A. x ph
4 1 simpri
 |-  ps
5 3 4 pm3.2i
 |-  ( A. x ph /\ ps )