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

Theorem ralimi 2724
Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralimi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ralimi  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )

Proof of Theorem ralimi
StepHypRef Expression
1 ralimi.1 . . 3  |-  ( ph  ->  ps )
21a1i 11 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32ralimia 2722 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   A.wral 2649
This theorem is referenced by:  ral2imi  2725  r19.26  2781  r19.29  2789  rr19.3v  3020  rr19.28v  3021  reu3  3067  uniiunlem  3374  reupick2  3570  uniss2  3988  ss2iun  4050  iineq2  4052  iunss2  4077  disjss2  4126  disjeq2  4127  reusv2lem5  4668  reusv3i  4670  tfis  4774  ssrel2  4906  issref  5187  dmmptg  5307  fununi  5457  fun11uni  5459  fnmpt  5511  fun11iun  5635  mpteqb  5758  chfnrn  5780  dffo5  5825  ffvresb  5839  fmptcof  5841  zfrep6  5907  mpt22eqb  6118  ralrnmpt2  6123  fnmpt2  6358  mpt2exxg  6361  frxp  6392  smores  6550  riiner  6913  ixpn0  7030  boxriin  7040  unifi2  7332  wemaplem2  7449  xpwdomg  7486  rankonidlem  7687  acni3  7861  dfac5  7942  dfac12lem2  7957  kmlem6  7968  kmlem8  7970  kmlem13  7975  cfsmolem  8083  fin23lem40  8164  isf32lem2  8167  fin1a2s  8227  hsmexlem2  8240  hsmex3  8247  axcc4  8252  domtriomlem  8255  dcomex  8260  ac6num  8292  iundom  8350  unirnfdomd  8375  konigthlem  8376  iunctb  8382  gch3  8488  wununi  8514  wunpw  8515  wunpr  8517  eltsk2g  8559  tskpwss  8560  tskpw  8561  grupw  8603  gruurn  8606  intgru  8622  grothpw  8634  grothpwex  8635  grothomex  8637  axgroth3  8639  suplem1pr  8862  supexpr  8864  supsr  8920  fimaxre3  9889  xrsupexmnf  10815  xrinfmexpnf  10816  rexanre  12077  rexuz3  12079  cau3lem  12085  caubnd2  12088  caubnd  12089  rlim0  12229  rlim0lt  12230  climi2  12232  climi0  12233  climrlim2  12268  rlimres  12279  o1rlimmul  12339  caurcvg  12397  caurcvg2  12398  caucvg  12399  caucvgb  12400  sumeq2  12415  ndvdssub  12854  gcdcllem1  12938  vdwnnlem1  13290  imasaddfnlem  13680  catidex  13826  catlid  13835  catrid  13836  catcocl  13837  catpropd  13862  subcidcl  13968  funcid  13994  setcepi  14170  tsrss  14582  laspwcl  14593  lanfwcl  14594  mgmidmo  14620  gsumval2  14710  issubg2  14886  gagrpid  14998  gaass  15001  dprdcntz  15493  dprddisj  15494  abveq0  15841  abvmul  15844  abvtri  15845  phllmhm  16786  ipcj  16788  ipeq0  16792  eltg2b  16947  iincld  17026  iuncld  17032  isclo2  17075  neips  17100  neipeltop  17116  lmcvg  17248  t1t0  17334  hauscmplem  17391  1stcelcls  17445  ptuni2  17529  pttopon  17549  ptcld  17566  ptcnplem  17574  txtube  17593  txlm  17601  xkococnlem  17612  fbun  17793  isfil2  17809  ptcmplem4  18007  tmdcn2  18040  ustssel  18156  isucn2  18230  ucncn  18236  xmeteq0  18277  xmettri2  18279  metrest  18444  tngngp  18566  iscau4  19103  cmetcaulem  19112  caussi  19121  volfiniun  19308  iunmbl  19314  voliun  19315  mbfdm  19387  itg2seq  19501  itg2i1fseqle  19513  itg2i1fseq2  19515  iblcnlem  19547  limcresi  19639  limciun  19648  rolle  19741  ulmss  20180  rlimcnp  20671  nbgraf1olem1  21317  isgrpo  21632  grpoidinv  21644  grpoideu  21645  grpoidval  21652  grpoidinv2  21654  opidon  21758  exidu1  21762  grpomndo  21782  rngoideu  21820  rngodi  21821  rngodir  21822  rngoass  21823  rngoueqz  21866  vcid  21878  vcdi  21879  vcdir  21880  vcass  21881  nvs  21999  nvz  22006  nvtri  22007  ajmoi  22208  adjmo  23183  cnlnssadj  23431  mdbr3  23648  mdbr4  23649  mdsl1i  23672  dmdbr6ati  23774  dmdbr7ati  23775  fnmptf  23916  hasheuni  24271  sigaclcu2  24299  prsiga  24310  measvunilem  24360  cntmeas  24374  cvmsdisj  24736  cvmshmeo  24737  cvmliftlem15  24764  cvmlift2lem12  24780  untangtr  24942  prodeq2  25019  elpotr  25161  dfon2lem7  25169  dfon2lem8  25170  tfisg  25228  wfisg  25233  frinsg  25269  poseq  25277  colinearalg  25563  axpasch  25594  axeuclid  25616  axcontlem2  25618  axcontlem4  25620  axcontlem7  25623  axcontlem8  25624  ovoliunnfl  25953  voliunnfl  25955  volsupnfl  25956  opnrebl2  26015  fnemeet2  26087  fnejoin1  26088  fnejoin2  26089  frinfm  26128  caushft  26158  sstotbnd3  26176  prdstotbnd  26194  heibor1lem  26209  bfplem2  26223  rngohomadd  26276  rngohommul  26277  idladdcl  26320  idllmulcl  26321  idlrmulcl  26322  ispridl2  26339  lerabdioph  26556  ltrabdioph  26559  nerabdioph  26560  dvdsrabdioph  26561  rencldnfi  26573  dford3  26790  ralbidar  27316  rexbidar  27317  stoweidlem60  27477  1to3vfriendship  27761  frconngra  27774  frgraregorufr0  27804  bnj1498  28768  pmapglbx  29883  ltrnnid  30250  cdlemefrs32fva  30514
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ral 2654
  Copyright terms: Public domain W3C validator