Metamath Proof Explorer

Theorem bj-genan

Description: Generalization rule on a conjunction. Forward inference associated with 19.26 . (Contributed by BJ, 7-Jul-2021)

Ref Expression
Hypothesis bj-genr.1 
|- ( ph /\ ps )
Assertion bj-genan 
|- ( A. x ph /\ A. x 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 4 ax-gen 
 |-  A. x ps
6 3 5 pm3.2i 
 |-  ( A. x ph /\ A. x ps )