Theorem bj-sblem2

Description: Lemma for substitution. (Contributed by BJ, 23-Jul-2023)

	Ref	Expression
Assertion	bj-sblem2	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜒 → 𝜓 ) ) → ( ( ∃ 𝑥 𝜑 → 𝜒 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		19.23v	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜒 ) ↔ ( ∃ 𝑥 𝜑 → 𝜒 ) )
2		ax-2	⊢ ( ( 𝜑 → ( 𝜒 → 𝜓 ) ) → ( ( 𝜑 → 𝜒 ) → ( 𝜑 → 𝜓 ) ) )
3	2	al2imi	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜒 → 𝜓 ) ) → ( ∀ 𝑥 ( 𝜑 → 𝜒 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )
4	1 3	syl5bir	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜒 → 𝜓 ) ) → ( ( ∃ 𝑥 𝜑 → 𝜒 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )