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

Theorem ralimi 2816
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 2814 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   A.wral 2773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-ral 2778
This theorem is referenced by:  ral2imiOLD  2818  r19.26  2953  r19.29  2961  rr19.3v  3210  rr19.28v  3211  reu3  3258  uniiunlem  3546  reupick2  3756  uniss2  4245  ss2iun  4309  iineq2  4311  iunss2  4338  disjss2  4391  disjeq2  4392  reusv2lem5  4622  reusv3i  4624  ssrel2  4937  issref  5225  dmmptg  5344  wfisg  5426  fununi  5659  fnmptf  5710  fnmpt  5714  mpteqb  5972  chfnrn  6000  fvn0ssdmfun  6020  dffo5  6046  ffvresb  6061  fmptcof  6064  mpt22eqb  6411  ralrnmpt2  6417  tfis  6687  fun11uni  6753  fun11iun  6759  zfrep6  6767  fnmpt2  6867  mpt2exxg  6873  frxp  6909  smores  7071  riiner  7436  ixpn0  7554  boxriin  7564  unifi2  7862  wemaplem2  8060  xpwdomg  8098  rankonidlem  8296  acni3  8474  dfac5  8555  dfac12lem2  8570  kmlem6  8581  kmlem8  8583  kmlem13  8588  cfsmolem  8696  fin23lem40  8777  isf32lem2  8780  fin1a2s  8840  hsmexlem2  8853  hsmex3  8860  axcc4  8865  domtriomlem  8868  dcomex  8873  ac6num  8905  iundom  8963  unirnfdomd  8988  konigthlem  8989  iunctb  8995  gch3  9097  wununi  9127  wunpw  9128  wunpr  9130  eltsk2g  9172  tskpwss  9173  tskpw  9174  grupw  9216  gruurn  9219  intgru  9235  grothpw  9247  grothpwex  9248  grothomex  9250  axgroth3  9252  suplem1pr  9473  supexpr  9475  supsr  9532  fimaxre3  10549  xrsupexmnf  11586  xrinfmexpnf  11587  fsuppmapnn0fiublem  12195  fsuppmapnn0fiub  12196  fsuppmapnn0fiubex  12197  mptnn0fsuppd  12203  rexanre  13388  rexuz3  13390  cau3lem  13396  caubnd2  13399  caubnd  13400  rlim0  13550  rlim0lt  13551  climi2  13553  climi0  13554  climrlim2  13589  rlimres  13600  o1rlimmul  13660  caurcvg  13720  caurcvgOLD  13721  caurcvg2  13722  caucvg  13723  caucvgb  13724  sumeq2  13738  prodeq2  13946  ndvdssub  14366  gcdcllem1  14451  coprmproddvdslem  14657  vdwnnlem1  14923  imasaddfnlem  15412  catidex  15558  catlid  15567  catrid  15568  catcocl  15569  catpropd  15592  subcidcl  15727  funcid  15753  setcepi  15961  tsrss  16447  mgmidmo  16480  gsumval2  16501  isnmnd  16518  issubg2  16810  gagrpid  16926  gaass  16929  dprdcntz  17618  dprddisj  17619  abveq0  18032  abvmul  18035  abvtri  18036  psgndiflemB  19145  phllmhm  19176  ipcj  19178  ipeq0  19182  mdetmul  19625  pmatcollpw2lem  19778  eltg2b  19951  iincld  20031  iuncld  20037  isclo2  20081  neips  20106  neipeltop  20122  lmcvg  20255  t1t0  20341  hauscmplem  20398  bwth  20402  1stcelcls  20453  ptuni2  20568  pttopon  20588  ptcld  20605  ptcnplem  20613  txtube  20632  txlm  20640  xkococnlem  20651  fbun  20832  isfil2  20848  ptcmplem4  21047  tmdcn2  21081  ustssel  21197  isucn2  21271  ucncn  21277  xmeteq0  21330  xmettri2  21332  metrest  21516  tngngp  21639  iscau4  22226  cmetcaulem  22235  caussi  22244  volfiniun  22477  iunmbl  22483  voliun  22484  mbfdm  22561  itg2seq  22677  itg2i1fseqle  22689  itg2i1fseq2  22691  iblcnlem  22723  limcresi  22817  limciun  22826  rolle  22919  ulmss  23329  rlimcnp  23868  midf  24795  colinearalg  24917  axpasch  24948  axeuclid  24970  axcontlem2  24972  axcontlem4  24974  axcontlem7  24977  axcontlem8  24978  nbgraf1olem1  25145  usgfiregdegfi  25615  1to3vfriendship  25712  frconngra  25725  frgraregorufr0  25756  usgreghash2spot  25773  isgrpo  25900  grpoidinv  25912  grpoideu  25913  grpoidval  25920  grpoidinv2  25922  opidonOLD  26026  exidu1  26030  grpomndo  26050  rngoideu  26088  rngodi  26089  rngodir  26090  rngoass  26091  rngoueqz  26134  vcid  26146  vcdi  26147  vcdir  26148  vcass  26149  nvs  26267  nvz  26274  nvtri  26275  ajmoi  26476  adjmo  27461  cnlnssadj  27709  mdbr3  27926  mdbr4  27927  mdsl1i  27950  dmdbr6ati  28052  dmdbr7ati  28053  disjunsn  28184  xrge0infssOLD  28326  hasheuni  28895  sigaclcu2  28931  prsiga  28942  measvunilem  29023  cntmeas  29037  omssubadd  29117  omssubaddOLD  29121  signsply0  29429  bnj1498  29859  cvmsdisj  29982  cvmshmeo  29983  cvmliftlem15  30010  cvmlift2lem12  30026  untangtr  30330  elpotr  30415  dfon2lem7  30423  dfon2lem8  30424  tfisg  30445  frinsg  30471  poseq  30479  opnrebl2  30963  fnemeet2  31009  fnejoin1  31010  fnejoin2  31011  ptrecube  31848  poimirlem25  31873  poimirlem26  31874  poimirlem27  31875  poimirlem30  31878  poimirlem31  31879  poimirlem32  31880  heicant  31883  ovoliunnfl  31890  voliunnfl  31892  volsupnfl  31893  frinfm  31970  caushft  31998  sstotbnd3  32016  prdstotbnd  32034  heibor1lem  32049  bfplem2  32063  rngohomadd  32116  rngohommul  32117  idladdcl  32160  idllmulcl  32161  idlrmulcl  32162  ispridl2  32179  mpt2bi123f  32314  iineq12f  32316  mptbi12f  32318  pmapglbx  33247  ltrnnid  33614  cdlemefrs32fva  33880  lerabdioph  35561  ltrabdioph  35564  nerabdioph  35565  dvdsrabdioph  35566  rencldnfi  35577  dford3  35797  pwelg  36078  pwinfi2  36080  ss2iundf  36105  ralbidar  36650  rexbidar  36651  stoweidlem60  37708  bgoldbtbndlem2  38521  bgoldbtbndlem4  38523  mpt2exxg2  39183
  Copyright terms: Public domain W3C validator