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

Theorem ralimi 3155
Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralimi.1 (𝜑𝜓)
Assertion
Ref Expression
ralimi (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)

Proof of Theorem ralimi
StepHypRef Expression
1 ralimi.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝑥𝐴 → (𝜑𝜓))
32ralimia 3153 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  wral 3133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-ral 3138
This theorem is referenced by:  2ralimi  3156  r19.26  3165  r19.29  3248  r19.30  3329  r19.35  3332  rr19.3v  3645  rr19.28v  3646  reu3  3704  uniiunlem  4047  reupick2  4274  uniss2  4857  ss2iun  4923  iineq2  4925  iunss2  4959  disjss2  5020  disjeq2  5021  triin  5173  reusv2lem5  5290  dmmptg  6083  wfisg  6170  fununi  6417  fnmptf  6473  fnmpt  6477  mpteqb  6778  chfnrn  6810  fvn0ssdmfun  6833  dffo5  6861  ffvresb  6879  fmptcof  6883  mpo2eqb  7276  ralrnmpo  7282  abnexg  7472  tfis  7563  fun11uni  7632  fiun  7639  f1iun  7640  zfrep6  7651  mpoexxg  7769  el2mpocsbcl  7776  frxp  7816  smores  7985  riiner  8366  ixpn0  8490  boxriin  8500  unifi2  8811  wemaplem2  9008  rankonidlem  9254  acni3  9471  dfac5  9552  dfac12lem2  9568  kmlem6  9579  kmlem8  9581  kmlem13  9586  cfsmolem  9690  fin23lem40  9771  isf32lem2  9774  fin1a2s  9834  hsmexlem2  9847  hsmex3  9854  axcc4  9859  domtriomlem  9862  dcomex  9867  ac6num  9899  iundom  9962  unirnfdomd  9987  konigthlem  9988  iunctb  9994  gch3  10096  wununi  10126  wunpw  10127  wunpr  10129  eltsk2g  10171  tskpwss  10172  tskpw  10173  grupw  10215  gruurn  10218  intgru  10234  grothpw  10246  grothpwex  10247  grothomex  10249  axgroth3  10251  suplem1pr  10472  supexpr  10474  supsr  10532  fimaxre3  11584  xrsupexmnf  12695  xrinfmexpnf  12696  fsuppmapnn0fiublem  13362  fsuppmapnn0fiub  13363  fsuppmapnn0fiubex  13364  mptnn0fsuppd  13370  rexanre  14706  rexuz3  14708  cau3lem  14714  caubnd2  14717  caubnd  14718  rlim0  14865  rlim0lt  14866  climi2  14868  climi0  14869  climrlim2  14904  rlimres  14915  o1rlimmul  14975  caurcvg  15033  caurcvg2  15034  caucvg  15035  caucvgb  15036  sumeq2  15051  prodeq2  15268  ndvdssub  15758  gcdcllem1  15846  coprmproddvdslem  16004  vdwnnlem1  16329  imasaddfnlem  16801  catidex  16945  catlid  16954  catrid  16955  catcocl  16956  catpropd  16979  subcidcl  17114  funcid  17140  setcepi  17348  tsrss  17833  mgmidmo  17870  gsumval2  17896  isnmnd  17915  issubg2  18294  gagrpid  18424  gaass  18427  cygabl  19010  dprdcntz  19130  dprddisj  19131  abveq0  19597  abvmul  19600  abvtri  19601  psgndiflemB  20296  phllmhm  20328  ipcj  20330  ipeq0  20334  mdetmul  21235  pmatcollpw2lem  21388  eltg2b  21570  iincld  21650  iuncld  21656  isclo2  21699  neips  21724  neipeltop  21740  lmcvg  21873  t1t0  21959  hauscmplem  22017  bwth  22021  1stcelcls  22072  ptuni2  22187  pttopon  22207  ptcld  22224  ptcnplem  22232  txtube  22251  txlm  22259  xkococnlem  22270  fbun  22451  isfil2  22467  ptcmplem4  22666  ustssel  22817  isucn2  22891  ucncn  22897  metrest  23137  tngngp  23266  tngngp3  23268  ncvsi  23762  iscau4  23889  cmetcaulem  23898  caussi  23907  volfiniun  24157  iunmbl  24163  voliun  24164  mbfdm  24236  itg2seq  24352  itg2i1fseqle  24364  itg2i1fseq2  24366  iblcnlem  24398  limcresi  24494  limciun  24503  rolle  24599  ulmss  24998  rlimcnp  25557  colinearalg  26710  axpasch  26741  axeuclid  26763  axcontlem2  26765  axcontlem4  26767  axcontlem7  26770  axcontlem8  26771  fusgrregdegfi  27365  0grrgr  27376  rusgr1vtxlem  27383  wlkvtxeledg  27419  wlkdlem3  27480  wlkdlem4  27481  lfgriswlk  27484  lfgrwlknloop  27485  eulercrct  28033  1to3vfriendship  28072  frgrregorufr0  28115  isgrpo  28286  grpoidinv  28297  grpoideu  28298  grpoidval  28302  grpoidinv2  28304  vcidOLD  28353  vcdi  28354  vcdir  28355  vcass  28356  nvs  28452  nvz  28458  nvtri  28459  mdbr3  30086  mdbr4  30087  mdsl1i  30110  dmdbr6ati  30212  dmdbr7ati  30213  disjunsn  30358  hasheuni  31404  sigaclcu2  31439  prsiga  31450  measvunilem  31531  cntmeas  31545  omssubadd  31618  signsply0  31881  bnj1498  32393  lfuhgr2  32425  cvmsdisj  32577  cvmshmeo  32578  cvmliftlem15  32605  cvmlift2lem12  32621  untangtr  33000  elpotr  33086  dfon2lem7  33094  dfon2lem8  33095  tfisg  33115  frpoinsg  33141  frinsg  33147  poseq  33155  opnrebl2  33729  fnemeet2  33775  fnejoin1  33776  fnejoin2  33777  dfgcd3  34686  domalom  34769  ctbssinf  34771  nlpfvineqsn  34774  fvineqsnf1  34775  pibt1  34781  pibt2  34782  ptrecube  35005  poimirlem25  35030  poimirlem26  35031  poimirlem27  35032  poimirlem30  35035  poimirlem31  35036  poimirlem32  35037  heicant  35040  ovoliunnfl  35047  voliunnfl  35049  volsupnfl  35050  frinfm  35121  caushft  35147  sstotbnd3  35162  prdstotbnd  35180  heibor1lem  35195  bfplem2  35209  opidonOLD  35238  exidu1  35242  grpomndo  35261  rngoideu  35289  rngodi  35290  rngodir  35291  rngoass  35292  rngoueqz  35326  idladdcl  35405  idllmulcl  35406  idlrmulcl  35407  mpobi123f  35548  iineq12f  35550  mptbi12f  35552  pmapglbx  37013  ltrnnid  37380  cdlemefrs32fva  37644  fsuppind  39393  dffltz  39535  lerabdioph  39666  ltrabdioph  39669  nerabdioph  39670  dvdsrabdioph  39671  rencldnfi  39682  dford3  39889  pwelg  40179  pwinfi2  40181  ss2iundf  40280  neik0imk0p  40662  gneispace  40760  gneispace0nelrn  40766  ralbidar  41073  rexbidar  41074  uzubico2  42137  climuzlem  42315  xlimxrre  42403  2reuimp0  43600  bgoldbtbndlem2  44254  bgoldbtbndlem4  44256  mpoexxg2  44669  iunord  45136
  Copyright terms: Public domain W3C validator