Theorem alsd 50626

Description: Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d 50628 and als2d 50629 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 50623	. 2 ⊢ (∀∃𝑥(𝜓 → 𝜒) ↔ (∀𝑥(𝜓 → 𝜒) ∧ ∃𝑥𝜓))
4	1, 2, 3	sylanbrc 595	1 ⊢ (𝜑 → ∀∃𝑥(𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  ∃wex 1812  ∀∃wals 50621

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-als 50623

This theorem is used by: (None)