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 φ ψ
Assertion bj-genl x φ ψ

Proof

Step Hyp Ref Expression
1 bj-genr.1 φ ψ
2 1 simpli φ
3 2 ax-gen x φ
4 1 simpri ψ
5 3 4 pm3.2i x φ ψ