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

Theorem ralimi 3099
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 3097 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2143  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883
This theorem depends on definitions:  df-bi 197  df-ral 3064
This theorem is referenced by:  2ralimi  3100  r19.26  3210  r19.29  3218  rr19.3v  3493  rr19.28v  3494  reu3  3545  uniiunlem  3838  reupick2  4058  uniss2  4603  ss2iun  4667  iineq2  4669  iunss2  4696  disjss2  4754  disjeq2  4755  reusv2lem5  5000  issref  5649  dmmptg  5775  wfisg  5857  fununi  6103  fnmptf  6155  fnmpt  6159  mpteqb  6440  chfnrn  6470  fvn0ssdmfun  6492  dffo5  6518  ffvresb  6535  fmptcof  6538  mpt22eqb  6914  ralrnmpt2  6920  abnexg  7109  tfis  7199  fun11uni  7265  fun11iun  7271  zfrep6  7279  mpt2exxg  7392  el2mpt2csbcl  7398  frxp  7436  smores  7600  riiner  7970  ixpn0  8092  boxriin  8102  unifi2  8410  wemaplem2  8606  rankonidlem  8853  acni3  9068  dfac5  9149  dfac12lem2  9166  kmlem6  9177  kmlem8  9179  kmlem13  9184  cfsmolem  9292  fin23lem40  9373  isf32lem2  9376  fin1a2s  9436  hsmexlem2  9449  hsmex3  9456  axcc4  9461  domtriomlem  9464  dcomex  9469  ac6num  9501  iundom  9564  unirnfdomd  9589  konigthlem  9590  iunctb  9596  gch3  9698  wununi  9728  wunpw  9729  wunpr  9731  eltsk2g  9773  tskpwss  9774  tskpw  9775  grupw  9817  gruurn  9820  intgru  9836  grothpw  9848  grothpwex  9849  grothomex  9851  axgroth3  9853  suplem1pr  10074  supexpr  10076  supsr  10133  fimaxre3  11170  xrsupexmnf  12339  xrinfmexpnf  12340  fsuppmapnn0fiublem  12996  fsuppmapnn0fiub  12997  fsuppmapnn0fiubOLD  12998  fsuppmapnn0fiubex  12999  mptnn0fsuppd  13005  rexanre  14297  rexuz3  14299  cau3lem  14305  caubnd2  14308  caubnd  14309  rlim0  14450  rlim0lt  14451  climi2  14453  climi0  14454  climrlim2  14489  rlimres  14500  o1rlimmul  14560  caurcvg  14618  caurcvg2  14619  caucvg  14620  caucvgb  14621  sumeq2  14635  prodeq2  14855  ndvdssub  15347  gcdcllem1  15435  coprmproddvdslem  15589  vdwnnlem1  15912  imasaddfnlem  16402  catidex  16548  catlid  16557  catrid  16558  catcocl  16559  catpropd  16582  subcidcl  16717  funcid  16743  setcepi  16951  tsrss  17437  mgmidmo  17473  gsumval2  17494  isnmnd  17512  issubg2  17823  gagrpid  17940  gaass  17943  dprdcntz  18621  dprddisj  18622  abveq0  19042  abvmul  19045  abvtri  19046  psgndiflemB  20168  phllmhm  20200  ipcj  20202  ipeq0  20206  mdetmul  20653  pmatcollpw2lem  20808  eltg2b  20990  iincld  21070  iuncld  21076  isclo2  21119  neips  21144  neipeltop  21160  lmcvg  21293  t1t0  21379  hauscmplem  21436  bwth  21440  1stcelcls  21491  ptuni2  21606  pttopon  21626  ptcld  21643  ptcnplem  21651  txtube  21670  txlm  21678  xkococnlem  21689  fbun  21870  isfil2  21886  ptcmplem4  22085  ustssel  22235  isucn2  22309  ucncn  22315  metrest  22555  tngngp  22684  tngngp3  22686  ncvsi  23176  iscau4  23302  cmetcaulem  23311  caussi  23320  volfiniun  23541  iunmbl  23547  voliun  23548  mbfdm  23620  itg2seq  23735  itg2i1fseqle  23747  itg2i1fseq2  23749  iblcnlem  23781  limcresi  23875  limciun  23884  rolle  23979  ulmss  24377  rlimcnp  24919  colinearalg  26017  axpasch  26048  axeuclid  26070  axcontlem2  26072  axcontlem4  26074  axcontlem7  26077  axcontlem8  26078  fusgrregdegfi  26706  0grrgr  26717  rusgr1vtxlem  26724  wlkvtxeledg  26760  wlkdlem3  26822  wlkdlem4  26823  lfgriswlk  26826  lfgrwlknloop  26827  eulercrct  27426  1to3vfriendship  27467  frgrregorufr0  27510  isgrpo  27692  grpoidinv  27703  grpoideu  27704  grpoidval  27708  grpoidinv2  27710  vcidOLD  27760  vcdi  27761  vcdir  27762  vcass  27763  nvs  27859  nvz  27865  nvtri  27866  mdbr3  29497  mdbr4  29498  mdsl1i  29521  dmdbr6ati  29623  dmdbr7ati  29624  disjunsn  29746  hasheuni  30488  sigaclcu2  30524  prsiga  30535  measvunilem  30616  cntmeas  30630  omssubadd  30703  signsply0  30969  bnj1498  31468  cvmsdisj  31591  cvmshmeo  31592  cvmliftlem15  31619  cvmlift2lem12  31635  untangtr  31930  elpotr  32023  dfon2lem7  32031  dfon2lem8  32032  tfisg  32053  frpoinsg  32079  frinsg  32083  poseq  32091  opnrebl2  32654  fnemeet2  32700  fnejoin1  32701  fnejoin2  32702  dfgcd3  33507  ptrecube  33742  poimirlem25  33767  poimirlem26  33768  poimirlem27  33769  poimirlem30  33772  poimirlem31  33773  poimirlem32  33774  heicant  33777  ovoliunnfl  33784  voliunnfl  33786  volsupnfl  33787  frinfm  33862  caushft  33889  sstotbnd3  33907  prdstotbnd  33925  heibor1lem  33940  bfplem2  33954  opidonOLD  33983  exidu1  33987  grpomndo  34006  rngoideu  34034  rngodi  34035  rngodir  34036  rngoass  34037  rngoueqz  34071  idladdcl  34150  idllmulcl  34151  idlrmulcl  34152  mpt2bi123f  34303  iineq12f  34305  mptbi12f  34307  pmapglbx  35577  ltrnnid  35944  cdlemefrs32fva  36209  lerabdioph  37895  ltrabdioph  37898  nerabdioph  37899  dvdsrabdioph  37900  rencldnfi  37911  dford3  38121  pwelg  38391  pwinfi2  38393  ss2iundf  38477  neik0imk0p  38860  gneispace  38958  gneispace0nelrn  38964  ralbidar  39175  rexbidar  39176  uzubico2  40316  climuzlem  40494  xlimxrre  40576  bgoldbtbndlem2  42219  bgoldbtbndlem4  42221  mpt2exxg2  42641  iunord  42947
  Copyright terms: Public domain W3C validator