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

Proof

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