Theorem wl-sbhbt

Description: Closed form of sbhb . Characterizing the expression ph -> A. x ph using a substitution expression. (Contributed by Wolf Lammen, 28-Jul-2019)

	Ref	Expression
Assertion	wl-sbhbt	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ∀ 𝑦 ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		wl-sb8t	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
2	1	imbi2d	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( 𝜑 → ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) )
3		19.21t	⊢ ( Ⅎ 𝑦 𝜑 → ( ∀ 𝑦 ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝜑 → ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) )
4	3	sps	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∀ 𝑦 ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝜑 → ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) )
5	2 4	bitr4d	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ∀ 𝑦 ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )