Metamath Proof Explorer

Theorem alan

Description: Alias for 19.26 for easier lookup. (Contributed by SN, 12-Aug-2025) (New usage is discouraged.)

Ref Expression
Assertion alan 
|- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) )

Proof

Step Hyp Ref Expression
1 19.26 
 |-  ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) )