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

Theorem alimdv 1709
Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1632. (Contributed by NM, 3-Apr-1994.)
Hypothesis
Ref Expression
alimdv.1
Assertion
Ref Expression
alimdv
Distinct variable group:   ,

Proof of Theorem alimdv
StepHypRef Expression
1 ax-5 1704 . 2
2 alimdv.1 . 2
31, 2alimdh 1638 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393
This theorem is referenced by:  2alimdv  1711  ax12v  1855  axc9lem1  2001  axc16i  2064  morimvOLD  2342  ralimdv2  2864  mo2icl  3278  sstr2  3510  reuss2  3777  ssuni  4271  disjss2  4425  disjss1  4428  disjiun  4442  disjss3  4451  alxfr  4665  frss  4851  ssrel  5096  ssrel2  5098  ssrelrel  5108  iotaval  5567  fvn0ssdmfun  6022  dff3  6044  dfwe2  6617  ordom  6709  findcard3  7783  dffi2  7903  indcardi  8443  zorn2lem4  8900  uzindi  12091  caubnd  13191  ramtlecl  14518  psgnunilem4  16522  bwthOLD  19911  dfcon2  19920  wilthlem3  23344  nbcusgra  24463  disjss1f  27435  ssrelf  27466  ss2mcls  28928  mclsax  28929  wzel  29380  onsuct0  29906  axc11next  31313  nrhmzr  32679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1618  ax-4 1631  ax-5 1704
  Copyright terms: Public domain W3C validator