Theorem alsd 50720

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

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

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 50717

This theorem is used by: (None)