Metamath Proof Explorer

Theorem bj-axdd2ALT

Description: Alternate proof of bj-axdd2 . (Contributed by BJ, 8-Mar-2026) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-axdd2ALT 
|- ( E. x ph -> ( A. x ps -> E. x ps ) )

Proof

Step Hyp Ref Expression
1 idd 
 |-  ( ph -> ( ps -> ps ) )
2 1 bj-exalimi 
 |-  ( E. x ph -> ( A. x ps -> E. x ps ) )