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

Theorem ralimi 2836
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 2834 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618
This theorem depends on definitions:  df-bi 185  df-ral 2798
This theorem is referenced by:  ral2imiOLD  2838  r19.26  2970  r19.29  2978  rr19.3v  3227  rr19.28v  3228  reu3  3275  uniiunlem  3573  reupick2  3769  uniss2  4267  ss2iun  4331  iineq2  4333  iunss2  4360  disjss2  4410  disjeq2  4411  reusv2lem5  4642  reusv3i  4644  ssrel2  5083  issref  5370  dmmptg  5494  fununi  5644  fnmpt  5697  mpteqb  5955  chfnrn  5983  fvn0ssdmfun  6007  dffo5  6033  ffvresb  6047  fmptcof  6050  mpt22eqb  6396  ralrnmpt2  6402  tfis  6674  fun11uni  6739  fun11iun  6745  zfrep6  6753  fnmpt2  6853  mpt2exxg  6859  frxp  6895  smores  7025  riiner  7386  ixpn0  7503  boxriin  7513  unifi2  7812  wemaplem2  7975  xpwdomg  8014  rankonidlem  8249  acni3  8431  dfac5  8512  dfac12lem2  8527  kmlem6  8538  kmlem8  8540  kmlem13  8545  cfsmolem  8653  fin23lem40  8734  isf32lem2  8737  fin1a2s  8797  hsmexlem2  8810  hsmex3  8817  axcc4  8822  domtriomlem  8825  dcomex  8830  ac6num  8862  iundom  8920  unirnfdomd  8945  konigthlem  8946  iunctb  8952  gch3  9057  wununi  9087  wunpw  9088  wunpr  9090  eltsk2g  9132  tskpwss  9133  tskpw  9134  grupw  9176  gruurn  9179  intgru  9195  grothpw  9207  grothpwex  9208  grothomex  9210  axgroth3  9212  suplem1pr  9433  supexpr  9435  supsr  9492  fimaxre3  10499  xrsupexmnf  11507  xrinfmexpnf  11508  fsuppmapnn0fiublem  12078  fsuppmapnn0fiub  12079  fsuppmapnn0fiubex  12080  mptnn0fsuppd  12086  rexanre  13161  rexuz3  13163  cau3lem  13169  caubnd2  13172  caubnd  13173  rlim0  13313  rlim0lt  13314  climi2  13316  climi0  13317  climrlim2  13352  rlimres  13363  o1rlimmul  13423  caurcvg  13481  caurcvg2  13482  caucvg  13483  caucvgb  13484  sumeq2  13498  prodeq2  13703  ndvdssub  14047  gcdcllem1  14131  vdwnnlem1  14495  imasaddfnlem  14907  catidex  15053  catlid  15062  catrid  15063  catcocl  15064  catpropd  15086  subcidcl  15192  funcid  15218  setcepi  15394  tsrss  15832  mgmidmo  15865  gsumval2  15886  isnmnd  15903  issubg2  16195  gagrpid  16311  gaass  16314  dprdcntz  17020  dprddisj  17021  abveq0  17454  abvmul  17457  abvtri  17458  psgndiflemB  18614  phllmhm  18645  ipcj  18647  ipeq0  18651  mdetmul  19103  pmatcollpw2lem  19256  eltg2b  19438  iincld  19518  iuncld  19524  isclo2  19567  neips  19592  neipeltop  19608  lmcvg  19741  t1t0  19827  hauscmplem  19884  bwth  19888  1stcelcls  19940  ptuni2  20055  pttopon  20075  ptcld  20092  ptcnplem  20100  txtube  20119  txlm  20127  xkococnlem  20138  fbun  20319  isfil2  20335  ptcmplem4  20533  tmdcn2  20566  ustssel  20686  isucn2  20760  ucncn  20766  xmeteq0  20819  xmettri2  20821  metrest  21005  tngngp  21146  iscau4  21696  cmetcaulem  21705  caussi  21714  volfiniun  21935  iunmbl  21941  voliun  21942  mbfdm  22013  itg2seq  22127  itg2i1fseqle  22139  itg2i1fseq2  22141  iblcnlem  22173  limcresi  22267  limciun  22276  rolle  22369  ulmss  22770  rlimcnp  23273  midf  24120  colinearalg  24191  axpasch  24222  axeuclid  24244  axcontlem2  24246  axcontlem4  24248  axcontlem7  24251  axcontlem8  24252  nbgraf1olem1  24419  usgfiregdegfi  24889  1to3vfriendship  24986  frconngra  24999  frgraregorufr0  25030  usgreghash2spot  25047  isgrpo  25176  grpoidinv  25188  grpoideu  25189  grpoidval  25196  grpoidinv2  25198  opidonOLD  25302  exidu1  25306  grpomndo  25326  rngoideu  25364  rngodi  25365  rngodir  25366  rngoass  25367  rngoueqz  25410  vcid  25422  vcdi  25423  vcdir  25424  vcass  25425  nvs  25543  nvz  25550  nvtri  25551  ajmoi  25752  adjmo  26729  cnlnssadj  26977  mdbr3  27194  mdbr4  27195  mdsl1i  27218  dmdbr6ati  27320  dmdbr7ati  27321  disjunsn  27431  fnmptf  27478  xrge0infss  27558  hasheuni  28069  sigaclcu2  28098  prsiga  28109  measvunilem  28161  cntmeas  28175  signsply0  28486  cvmsdisj  28693  cvmshmeo  28694  cvmliftlem15  28721  cvmlift2lem12  28737  untangtr  29064  elpotr  29189  dfon2lem7  29197  dfon2lem8  29198  tfisg  29260  wfisg  29265  frinsg  29301  poseq  29309  heicant  30025  ovoliunnfl  30032  voliunnfl  30034  volsupnfl  30035  opnrebl2  30115  fnemeet2  30161  fnejoin1  30162  fnejoin2  30163  frinfm  30202  caushft  30230  sstotbnd3  30248  prdstotbnd  30266  heibor1lem  30281  bfplem2  30295  rngohomadd  30348  rngohommul  30349  idladdcl  30392  idllmulcl  30393  idlrmulcl  30394  ispridl2  30411  mpt2bi123f  30547  iineq12f  30549  mptbi12f  30551  lerabdioph  30714  ltrabdioph  30717  nerabdioph  30718  dvdsrabdioph  30719  rencldnfi  30731  dford3  30946  ralbidar  31308  rexbidar  31309  stoweidlem60  31796  mpt2exxg2  32795  bnj1498  33985  pmapglbx  35368  ltrnnid  35735  cdlemefrs32fva  36001  pwelg  37583  pwinfi2  37585
  Copyright terms: Public domain W3C validator