Metamath Proof Explorer

Theorem alim

Description: Restatement of Axiom ax-4 , for labeling consistency. It should be the only theorem using ax-4 . (Contributed by NM, 10-Jan-1993)

Ref Expression
Assertion alim 
|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )

Proof

Step Hyp Ref Expression
1 ax-4 
 |-  ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )