Theorem alsd 50569

Description: Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d 50571 and als2d 50572 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.)

Hypotheses

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

Assertion

Ref	Expression
alsd	⊢ (𝜑 → ∀∃𝑥(𝜓 → 𝜒))

Proof of Theorem alsd

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

Syntax hints:   → wi 4  ∀wal 1568  ∃wex 1809  ∀∃wals 50564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401  df-als 50566

This theorem is referenced by: (None)