Theorem alsd 17229

Description: Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d 17231 and als2d 17232 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	|- ( ph -> A. x ( ps -> ch ) )
alsd.2	|- ( ph -> E. x ps )

Assertion

Ref	Expression
alsd	|- ( ph -> A.E. x ( ps -> ch ) )

Proof of Theorem alsd

Step	Hyp	Ref	Expression
1		alsd.1	. 2 |- ( ph -> A. x ( ps -> ch ) )
2		alsd.2	. 2 |- ( ph -> E. x ps )
3		df-als 17226	. 2 |- ( A.E. x ( ps -> ch ) <-> ( A. x ( ps -> ch ) /\ E. x ps ) )
4	1, 2, 3	sylanbrc 421	1 |- ( ph -> A.E. x ( ps -> ch ) )

This proof depends on syntax axioms:   -> wi 4   A.wal 1400   E.wex 1545   A.E.wals 17224

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-als 17226

This theorem is used by: (None)