Theorem alsd 51315

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

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

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 51312

This theorem is used by: (None)