Theorem alsd

Description: Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d and als2d taken together, and is what lets an "all some" statement be proved rather than merely taken apart. (Contributed by David A. Wheeler, 12-Jul-2026)

	Ref	Expression
Hypotheses	alsd.1	⊢ ( 𝜑 → ∀ 𝑥 ( 𝜓 → 𝜒 ) )
	alsd.2	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
Assertion	alsd	⊢ ( 𝜑 → ∀∃ 𝑥 ( 𝜓 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		alsd.1	⊢ ( 𝜑 → ∀ 𝑥 ( 𝜓 → 𝜒 ) )
2		alsd.2	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
3		df-als	⊢ ( ∀∃ 𝑥 ( 𝜓 → 𝜒 ) ↔ ( ∀ 𝑥 ( 𝜓 → 𝜒 ) ∧ ∃ 𝑥 𝜓 ) )
4	1 2 3	sylanbrc	⊢ ( 𝜑 → ∀∃ 𝑥 ( 𝜓 → 𝜒 ) )