MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alim Unicode version

Theorem alim 1632
Description: Restatement of Axiom ax-4 1631, for labelling consistency. It should be the only theorem using ax-4 1631. (Contributed by NM, 10-Jan-1993.)
Assertion
Ref Expression
alim

Proof of Theorem alim
StepHypRef Expression
1 ax-4 1631 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393
This theorem is referenced by:  alimi  1633  al2im  1635  19.21v  1729  spfw  1806  axc4  1860  19.21t  1904  eunex  4645  hbaltg  29240  hbalg  33328  al2imVD  33662  hbalgVD  33705  bj-2alim  34202  bj-alrimh  34208  bj-hbalt  34240  bj-nfdt0  34248  bj-eunex  34385  stdpc5t  34400  al3im  37766
This theorem was proved from axioms:  ax-4 1631
  Copyright terms: Public domain W3C validator