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

Theorem ralimi 2949
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 2947 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  wral 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-ral 2914
This theorem is referenced by:  2ralimi  2950  r19.26  3060  r19.29  3068  rr19.3v  3339  rr19.28v  3340  reu3  3390  uniiunlem  3683  reupick2  3905  uniss2  4461  ss2iun  4527  iineq2  4529  iunss2  4556  disjss2  4614  disjeq2  4615  reusv2lem5  4864  issref  5497  dmmptg  5620  wfisg  5703  fununi  5952  fnmptf  6003  fnmpt  6007  mpteqb  6285  chfnrn  6314  fvn0ssdmfun  6336  dffo5  6362  ffvresb  6380  fmptcof  6383  mpt22eqb  6754  ralrnmpt2  6760  abnexg  6949  tfis  7039  fun11uni  7105  fun11iun  7111  zfrep6  7119  mpt2exxg  7229  el2mpt2csbcl  7235  frxp  7272  smores  7434  riiner  7805  ixpn0  7925  boxriin  7935  unifi2  8241  wemaplem2  8437  rankonidlem  8676  acni3  8855  dfac5  8936  dfac12lem2  8951  kmlem6  8962  kmlem8  8964  kmlem13  8969  cfsmolem  9077  fin23lem40  9158  isf32lem2  9161  fin1a2s  9221  hsmexlem2  9234  hsmex3  9241  axcc4  9246  domtriomlem  9249  dcomex  9254  ac6num  9286  iundom  9349  unirnfdomd  9374  konigthlem  9375  iunctb  9381  gch3  9483  wununi  9513  wunpw  9514  wunpr  9516  eltsk2g  9558  tskpwss  9559  tskpw  9560  grupw  9602  gruurn  9605  intgru  9621  grothpw  9633  grothpwex  9634  grothomex  9636  axgroth3  9638  suplem1pr  9859  supexpr  9861  supsr  9918  fimaxre3  10955  xrsupexmnf  12120  xrinfmexpnf  12121  fsuppmapnn0fiublem  12772  fsuppmapnn0fiub  12773  fsuppmapnn0fiubOLD  12774  fsuppmapnn0fiubex  12775  mptnn0fsuppd  12781  rexanre  14067  rexuz3  14069  cau3lem  14075  caubnd2  14078  caubnd  14079  rlim0  14220  rlim0lt  14221  climi2  14223  climi0  14224  climrlim2  14259  rlimres  14270  o1rlimmul  14330  caurcvg  14388  caurcvg2  14389  caucvg  14390  caucvgb  14391  sumeq2  14405  prodeq2  14625  ndvdssub  15114  gcdcllem1  15202  coprmproddvdslem  15357  vdwnnlem1  15680  imasaddfnlem  16169  catidex  16316  catlid  16325  catrid  16326  catcocl  16327  catpropd  16350  subcidcl  16485  funcid  16511  setcepi  16719  tsrss  17204  mgmidmo  17240  gsumval2  17261  isnmnd  17279  issubg2  17590  gagrpid  17708  gaass  17711  dprdcntz  18388  dprddisj  18389  abveq0  18807  abvmul  18810  abvtri  18811  psgndiflemB  19927  phllmhm  19958  ipcj  19960  ipeq0  19964  mdetmul  20410  pmatcollpw2lem  20563  eltg2b  20744  iincld  20824  iuncld  20830  isclo2  20873  neips  20898  neipeltop  20914  lmcvg  21047  t1t0  21133  hauscmplem  21190  bwth  21194  1stcelcls  21245  ptuni2  21360  pttopon  21380  ptcld  21397  ptcnplem  21405  txtube  21424  txlm  21432  xkococnlem  21443  fbun  21625  isfil2  21641  ptcmplem4  21840  ustssel  21990  isucn2  22064  ucncn  22070  metrest  22310  tngngp  22439  tngngp3  22441  ncvsi  22932  iscau4  23058  cmetcaulem  23067  caussi  23076  volfiniun  23296  iunmbl  23302  voliun  23303  mbfdm  23376  itg2seq  23490  itg2i1fseqle  23502  itg2i1fseq2  23504  iblcnlem  23536  limcresi  23630  limciun  23639  rolle  23734  ulmss  24132  rlimcnp  24673  colinearalg  25771  axpasch  25802  axeuclid  25824  axcontlem2  25826  axcontlem4  25828  axcontlem7  25831  axcontlem8  25832  fusgrregdegfi  26446  0grrgr  26457  rusgr1vtxlem  26464  wlkvtxeledg  26500  wlkdlem3  26562  wlkdlem4  26563  lfgriswlk  26566  lfgrwlknloop  26567  eulercrct  27082  1to3vfriendship  27125  frgrregorufr0  27162  isgrpo  27321  grpoidinv  27332  grpoideu  27333  grpoidval  27337  grpoidinv2  27339  vcidOLD  27389  vcdi  27390  vcdir  27391  vcass  27392  nvs  27488  nvz  27494  nvtri  27495  mdbr3  29126  mdbr4  29127  mdsl1i  29150  dmdbr6ati  29252  dmdbr7ati  29253  disjunsn  29379  hasheuni  30121  sigaclcu2  30157  prsiga  30168  measvunilem  30249  cntmeas  30263  omssubadd  30336  signsply0  30602  bnj1498  31103  cvmsdisj  31226  cvmshmeo  31227  cvmliftlem15  31254  cvmlift2lem12  31270  untangtr  31565  elpotr  31660  dfon2lem7  31668  dfon2lem8  31669  tfisg  31690  frinsg  31716  poseq  31724  opnrebl2  32291  fnemeet2  32337  fnejoin1  32338  fnejoin2  32339  dfgcd3  33141  ptrecube  33380  poimirlem25  33405  poimirlem26  33406  poimirlem27  33407  poimirlem30  33410  poimirlem31  33411  poimirlem32  33412  heicant  33415  ovoliunnfl  33422  voliunnfl  33424  volsupnfl  33425  frinfm  33501  caushft  33528  sstotbnd3  33546  prdstotbnd  33564  heibor1lem  33579  bfplem2  33593  opidonOLD  33622  exidu1  33626  grpomndo  33645  rngoideu  33673  rngodi  33674  rngodir  33675  rngoass  33676  rngoueqz  33710  idladdcl  33789  idllmulcl  33790  idlrmulcl  33791  mpt2bi123f  33942  iineq12f  33944  mptbi12f  33946  pmapglbx  34874  ltrnnid  35241  cdlemefrs32fva  35507  lerabdioph  37188  ltrabdioph  37191  nerabdioph  37192  dvdsrabdioph  37193  rencldnfi  37204  dford3  37414  pwelg  37684  pwinfi2  37686  ss2iundf  37770  neik0imk0p  38154  gneispace  38252  gneispace0nelrn  38258  ralbidar  38469  rexbidar  38470  uzubico2  39600  climuzlem  39775  bgoldbtbndlem2  41459  bgoldbtbndlem4  41461  mpt2exxg2  41881  iunord  42187
  Copyright terms: Public domain W3C validator