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	$$⊢\left(\phi \wedge \psi \right)$$
Assertion	bj-genan	$$⊢\left(\forall x\phi \wedge \forall x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-genr.1	$$⊢\left(\phi \wedge \psi \right)$$
2	1	simpli	$$⊢\phi$$
3	2	ax-gen	$$⊢\forall x\phi$$
4	1	simpri	$$⊢\psi$$
5	4	ax-gen	$$⊢\forall x\psi$$
6	3 5	pm3.2i	$$⊢\left(\forall x\phi \wedge \forall x\psi \right)$$