Theorem alim 1738

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

Assertion

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

Proof of Theorem alim

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

Syntax hints:   -> wi 4   A.wal 1481

This theorem was proved from axioms:  ax-4 1737

This theorem is referenced by:  alimi  1739  al2im  1742  sylgt  1749  19.38a  1767  stdpc5v  1867  spfwOLD  1966  19.21tOLDOLD  2074  axc4  2130  19.21t-1OLD  2212  eunex  4859  hbaltg  31713  bj-2alim  32594  bj-alexim  32605  bj-hbalt  32671  bj-nfdt0  32685  bj-eunex  32799  stdpc5t  32814  al3im  37938  hbalg  38771  al2imVD  39098  hbalgVD  39141