Theorem bj-hbsb3

Description: Shorter proof of hbsb3 . (Contributed by BJ, 2-May-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	bj-hbsb3.1	|- ( ph -> A. y ph )
Assertion	bj-hbsb3	|- ( [ y / x ] ph -> A. x [ y / x ] ph )

Proof

Step	Hyp	Ref	Expression
1		bj-hbsb3.1	|- ( ph -> A. y ph )
2		bj-hbsb3t	|- ( A. x ( ph -> A. y ph ) -> ( [ y / x ] ph -> A. x [ y / x ] ph ) )
3	2 1	mpg	|- ( [ y / x ] ph -> A. x [ y / x ] ph )