Theorem alsd 50856

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

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

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 50853

This theorem is used by: (None)