Theorem bj-sblem

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

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

Proof

Step	Hyp	Ref	Expression
1		pm5.74	⊢ ( ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜒 ) ) )
2	1	albii	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) ↔ ∀ 𝑥 ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜒 ) ) )
3		albi	⊢ ( ∀ 𝑥 ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜒 ) ) → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 → 𝜒 ) ) )
4	2 3	sylbi	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 → 𝜒 ) ) )
5		19.23v	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜒 ) ↔ ( ∃ 𝑥 𝜑 → 𝜒 ) )
6	4 5	bitrdi	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 𝜑 → 𝜒 ) ) )