Theorem bj-hbsb3

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

	Ref	Expression
Hypothesis	bj-hbsb3.1	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
Assertion	bj-hbsb3	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		bj-hbsb3.1	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
2		bj-hbsb3t	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜑 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 ) )
3	2 1	mpg	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 )