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 ( 𝜑𝜓 )
Assertion bj-genan ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 )

Proof

Step Hyp Ref Expression
1 bj-genr.1 ( 𝜑𝜓 )
2 1 simpli 𝜑
3 2 ax-gen 𝑥 𝜑
4 1 simpri 𝜓
5 4 ax-gen 𝑥 𝜓
6 3 5 pm3.2i ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 )