Theorem ralimi 3108

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

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	ralimia 3105	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836

This theorem depends on definitions:  df-bi 210  df-ral 3086

This theorem is referenced by:  rexbi  3127  ralrexbid  3128  r19.26  3131  r19.30  3138  2ralimi  3141  3ralimi  3142  4ralimi  3143  5ralimi  3144  6ralimi  3145  r19.21v  3196  rr19.3v  3635  rr19.28v  3636  reu3  3699  uniiunlem  4049  reupick2  4292  uniss2  4908  ss2iun  4976  iineq2  4978  dfiun2g  4995  iunss2  5015  disjss2  5080  disjeq2  5081  triin  5236  replem  5250  zfrep6  5251  reusv2lem5  5371  dmmptg  6240  frpoinsg  6341  fununi  6608  fnmptf  6669  fnmpt  6673  mpteqb  7007  chfnrn  7042  fvn0ssdmfun  7067  dffo5  7097  ffvresb  7119  fmptcof  7124  mpo2eqb  7540  ralrnmpo  7547  abnexg  7751  tfisg  7846  tfis  7847  fun11uni  7926  fiun  7936  f1iun  7937  zfrep6OLD  7948  mpoexxg  8068  el2mpocsbcl  8076  frxp  8118  xpord2indlem  8139  xpord3inddlem  8146  poseq  8150  smores  8335  naddcllem  8658  naddcom  8665  naddrid  8666  naddunif  8676  naddass  8679  riiner  8784  ixpn0  8924  boxriin  8934  unifi2  9298  wemaplem2  9505  frinsg  9719  rankonidlem  9796  acni3  10027  dfac5  10108  dfac12lem2  10124  kmlem6  10135  kmlem8  10137  kmlem13  10142  cfsmolem  10250  fin23lem40  10331  isf32lem2  10334  fin1a2s  10394  hsmexlem2  10407  hsmex3  10414  axcc4  10419  domtriomlem  10422  dcomex  10427  ac6num  10459  iundom  10522  unirnfdomd  10548  konigthlem  10549  iunctb  10555  gch3  10657  wununi  10687  wunpw  10688  wunpr  10690  eltsk2g  10732  tskpwss  10733  tskpw  10734  grupw  10776  gruurn  10779  intgru  10795  grothpw  10807  grothpwex  10808  grothomex  10810  axgroth3  10812  suplem1pr  11033  supexpr  11035  supsr  11093  fimaxre3  12157  xrsupexmnf  13327  xrinfmexpnf  13328  fsuppmapnn0fiublem  14022  fsuppmapnn0fiub  14023  fsuppmapnn0fiubex  14024  mptnn0fsuppd  14030  rexanre  15394  rexuz3  15396  cau3lem  15402  caubnd2  15405  caubnd  15406  rlim0  15555  rlim0lt  15556  climi2  15558  climi0  15559  climrlim2  15594  rlimres  15605  o1rlimmul  15666  caurcvg  15724  caurcvg2  15725  caucvg  15726  caucvgb  15727  sumeq2  15741  prodeq2  15962  ndvdssub  16463  gcdcllem1  16553  coprmproddvdslem  16716  vdwnnlem1  17051  imasaddfnlem  17578  catidex  17726  catlid  17735  catrid  17736  catcocl  17737  catpropd  17761  subcidcl  17897  funcid  17923  setcepi  18141  tsrss  18641  mgmidmo  18714  gsumval2  18740  isnmnd  18792  issubg2  19204  gagrpid  19360  gaass  19363  cygabl  19957  dprdcntz  20076  dprddisj  20077  abveq0  20895  abvmul  20898  abvtri  20899  psgndiflemB  21715  phllmhm  21747  ipcj  21749  ipeq0  21753  mdetmul  22745  pmatcollpw2lem  22899  eltg2b  23081  iincld  23161  iuncld  23167  isclo2  23210  neips  23235  neipeltop  23251  lmcvg  23384  t1t0  23470  hauscmplem  23528  bwth  23532  1stcelcls  23583  ptuni2  23698  pttopon  23718  ptcld  23735  ptcnplem  23743  txtube  23762  txlm  23770  xkococnlem  23781  fbun  23962  isfil2  23978  ptcmplem4  24177  ustssel  24328  isucn2  24400  ucncn  24406  metrest  24646  tngngp  24776  tngngp3  24778  ncvsi  25275  iscau4  25403  cmetcaulem  25412  caussi  25421  volfiniun  25671  iunmbl  25677  voliun  25678  mbfdm  25750  itg2seq  25866  itg2i1fseqle  25878  itg2i1fseq2  25880  iblcnlem  25913  limcresi  26009  limciun  26018  rolle  26114  ulmss  26522  rlimcnp  27092  madebdayim  28043  addsuniflem  28156  oldfib  28532  colinearalg  29197  axpasch  29228  axeuclid  29250  axcontlem2  29252  axcontlem4  29254  axcontlem7  29257  axcontlem8  29258  fusgrregdegfi  29856  0grrgr  29867  rusgr1vtxlem  29874  wlkvtxeledg  29910  wlkdlem3  29969  wlkdlem4  29970  lfgriswlk  29973  lfgrwlknloop  29974  eulercrct  30530  1to3vfriendship  30569  frgrregorufr0  30612  isgrpo  30786  grpoidinv  30797  grpoideu  30798  grpoidval  30802  grpoidinv2  30804  vcidOLD  30853  vcdi  30854  vcdir  30855  vcass  30856  nvs  30952  nvz  30958  nvtri  30959  mdbr3  32586  mdbr4  32587  mdsl1i  32610  dmdbr6ati  32712  dmdbr7ati  32713  disjunsn  32876  hasheuni  34416  sigaclcu2  34451  prsiga  34462  measvunilem  34543  cntmeas  34557  omssubadd  34631  signsply0  34879  bnj1498  35390  nummin  35423  axprALT2  35441  tz9.1regs  35466  onvf1odlem4  35485  lfuhgr2  35506  cvmsdisj  35657  cvmshmeo  35658  cvmliftlem15  35685  cvmlift2lem12  35701  untangtr  36101  elpotr  36166  dfon2lem7  36174  dfon2lem8  36175  nmulprop  36577  opnrebl2  36717  fnemeet2  36763  fnejoin1  36764  fnejoin2  36765  weiunso  36862  weiunse  36864  weiunwe  36865  dfgcd3  37851  domalom  37933  ctbssinf  37935  nlpfvineqsn  37938  fvineqsnf1  37939  pibt1  37945  pibt2  37946  ptrecube  38154  poimirlem25  38179  poimirlem26  38180  poimirlem27  38181  poimirlem30  38184  poimirlem31  38185  poimirlem32  38186  heicant  38189  ovoliunnfl  38196  voliunnfl  38198  volsupnfl  38199  frinfm  38269  caushft  38295  sstotbnd3  38310  prdstotbnd  38328  heibor1lem  38343  bfplem2  38357  opidonOLD  38386  exidu1  38390  grpomndo  38409  rngoideu  38437  rngodi  38438  rngodir  38439  rngoass  38440  rngoueqz  38474  idladdcl  38553  idllmulcl  38554  idlrmulcl  38555  mpobi123f  38696  iineq12f  38698  mptbi12f  38700  dmqsblocks  39501  pmapglbx  40428  ltrnnid  40795  cdlemefrs32fva  41059  unitscyglem3  42849  fsuppind  43207  dffltz  43251  lerabdioph  43417  ltrabdioph  43420  nerabdioph  43421  dvdsrabdioph  43422  rencldnfi  43433  dford3  43640  pwelg  44171  pwinfi2  44173  ss2iundf  44270  neik0imk0p  44647  gneispace  44745  gneispace0nelrn  44751  ismnushort  44896  ralbidar  45039  rexbidar  45040  ssclaxsep  45576  uniclaxun  45580  uzubico2  46169  climuzlem  46342  xlimxrre  46430  natlocalincr  47477  2reuimp0  47733  bgoldbtbndlem2  48453  bgoldbtbndlem4  48455  mpoexxg2  48996  iuneqconst2  49479  iineqconst2  49480  iunord  50332