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

Theorem ralimdv 2835
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)
Hypothesis
Ref Expression
ralimdv.1
Assertion
Ref Expression
ralimdv
Distinct variable group:   ,

Proof of Theorem ralimdv
StepHypRef Expression
1 ralimdv.1 . . 3
21adantr 465 . 2
32ralimdva 2833 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1758  A.wral 2800
This theorem is referenced by:  poss  4760  sess1  4805  sess2  4806  riinint  5213  iinpreima  5956  dffo4  5982  dffo5  5983  isoini2  6161  tfindsg  6604  iiner  7306  xpf1o  7607  dffi3  7817  brwdom3  7934  xpwdomg  7937  bndrank  8185  cfub  8555  cff1  8564  cfflb  8565  cfslb2n  8574  cofsmo  8575  cfcoflem  8578  pwcfsdom  8884  fpwwe2lem13  8946  inawinalem  8993  grupr  9101  fsequb  11942  cau3lem  13000  caubnd2  13003  caubnd  13004  rlim2lt  13133  rlim3  13134  climshftlem  13210  isercolllem1  13300  climcau  13306  caucvgb  13315  serf0  13316  cvgcmp  13437  mreriincl  14695  acsfn1c  14759  islss4  17219  riinopn  18920  fiinbas  18956  baspartn  18958  isclo2  19091  lmcls  19305  lmcnp  19307  isnrm3  19362  1stcelcls  19464  llyss  19482  nllyss  19483  ptpjpre1  19543  txlly  19608  txnlly  19609  tx1stc  19622  xkococnlem  19631  fbunfip  19841  filssufilg  19883  cnpflf2  19972  fcfnei  20007  isucn2  20253  rescncf  20872  lebnum  20935  cfilss  21180  fgcfil  21181  iscau4  21189  cmetcaulem  21198  cfilres  21206  caussi  21207  ovolunlem1  21379  ulmclm  22252  ulmcaulem  22259  ulmcau  22260  ulmss  22262  rlimcnp  22759  cxploglim  22771  lgsdchr  23087  pntlemp  23259  axcontlem4  23682  nmlnoubi  24665  lnon0  24667  disjpreima  26396  resspos  26581  resstos  26582  submarchi  26664  iccllyscon  27595  cvmlift2lem1  27647  setlikess  28112  upixp  29083  caushft  29117  sstotbnd3  29135  totbndss  29136  unichnidl  29291  ispridl2  29298  elrfirn2  29492  mzpsubst  29545  eluzrabdioph  29604  fourierdlem103  30739  fourierdlem104  30740  ralralimp  30996  modfsummods  31121  usg2wlkeq  31166  3cyclfrgrarn2  31483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2805
  Copyright terms: Public domain W3C validator