Theorem ralimi 3076

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 3073	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2119  ∀wral 3053

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

This theorem depends on definitions:  df-bi 208  df-ral 3054

This theorem is referenced by:  rexbi  3095  ralrexbid  3096  r19.26  3099  r19.30  3106  2ralimi  3109  3ralimi  3110  4ralimi  3111  5ralimi  3112  6ralimi  3113  r19.21v  3164  rr19.3v  3605  rr19.28v  3606  reu3  3668  uniiunlem  4018  reupick2  4259  uniss2  4872  ss2iun  4940  iineq2  4942  dfiun2g  4959  iunss2  4979  disjss2  5042  disjeq2  5043  triin  5196  replem  5210  zfrep6  5211  reusv2lem5  5331  dmmptg  6193  frpoinsg  6294  fununi  6560  fnmptf  6621  fnmpt  6625  mpteqb  6955  chfnrn  6990  fvn0ssdmfun  7015  dffo5  7045  ffvresb  7067  fmptcof  7072  mpo2eqb  7488  ralrnmpo  7495  abnexg  7699  tfisg  7794  tfis  7795  fun11uni  7873  fiun  7885  f1iun  7886  zfrep6OLD  7897  mpoexxg  8017  el2mpocsbcl  8024  frxp  8066  xpord2indlem  8087  xpord3inddlem  8094  poseq  8098  smores  8282  naddcllem  8602  naddcom  8608  naddrid  8609  naddunif  8619  naddass  8622  riiner  8727  ixpn0  8868  boxriin  8878  unifi2  9245  wemaplem2  9452  frinsg  9666  rankonidlem  9743  acni3  9960  dfac5  10042  dfac12lem2  10058  kmlem6  10069  kmlem8  10071  kmlem13  10076  cfsmolem  10183  fin23lem40  10264  isf32lem2  10267  fin1a2s  10327  hsmexlem2  10340  hsmex3  10347  axcc4  10352  domtriomlem  10355  dcomex  10360  ac6num  10392  iundom  10455  unirnfdomd  10481  konigthlem  10482  iunctb  10488  gch3  10590  wununi  10620  wunpw  10621  wunpr  10623  eltsk2g  10665  tskpwss  10666  tskpw  10667  grupw  10709  gruurn  10712  intgru  10728  grothpw  10740  grothpwex  10741  grothomex  10743  axgroth3  10745  suplem1pr  10966  supexpr  10968  supsr  11026  fimaxre3  12093  xrsupexmnf  13248  xrinfmexpnf  13249  fsuppmapnn0fiublem  13943  fsuppmapnn0fiub  13944  fsuppmapnn0fiubex  13945  mptnn0fsuppd  13951  rexanre  15300  rexuz3  15302  cau3lem  15308  caubnd2  15311  caubnd  15312  rlim0  15461  rlim0lt  15462  climi2  15464  climi0  15465  climrlim2  15500  rlimres  15511  o1rlimmul  15572  caurcvg  15630  caurcvg2  15631  caucvg  15632  caucvgb  15633  sumeq2  15647  prodeq2  15868  ndvdssub  16369  gcdcllem1  16459  coprmproddvdslem  16622  vdwnnlem1  16957  imasaddfnlem  17483  catidex  17631  catlid  17640  catrid  17641  catcocl  17642  catpropd  17666  subcidcl  17802  funcid  17828  setcepi  18046  tsrss  18546  mgmidmo  18619  gsumval2  18645  isnmnd  18697  issubg2  19108  gagrpid  19260  gaass  19263  cygabl  19857  dprdcntz  19976  dprddisj  19977  abveq0  20790  abvmul  20793  abvtri  20794  psgndiflemB  21575  phllmhm  21607  ipcj  21609  ipeq0  21613  mdetmul  22606  pmatcollpw2lem  22760  eltg2b  22942  iincld  23022  iuncld  23028  isclo2  23071  neips  23096  neipeltop  23112  lmcvg  23245  t1t0  23331  hauscmplem  23389  bwth  23393  1stcelcls  23444  ptuni2  23559  pttopon  23579  ptcld  23596  ptcnplem  23604  txtube  23623  txlm  23631  xkococnlem  23642  fbun  23823  isfil2  23839  ptcmplem4  24038  ustssel  24189  isucn2  24261  ucncn  24267  metrest  24507  tngngp  24637  tngngp3  24639  ncvsi  25136  iscau4  25264  cmetcaulem  25273  caussi  25282  volfiniun  25532  iunmbl  25538  voliun  25539  mbfdm  25611  itg2seq  25727  itg2i1fseqle  25739  itg2i1fseq2  25741  iblcnlem  25774  limcresi  25870  limciun  25879  rolle  25975  ulmss  26380  rlimcnp  26947  madebdayim  27898  addsuniflem  28011  oldfib  28387  colinearalg  28997  axpasch  29028  axeuclid  29050  axcontlem2  29052  axcontlem4  29054  axcontlem7  29057  axcontlem8  29058  fusgrregdegfi  29656  0grrgr  29667  rusgr1vtxlem  29674  wlkvtxeledg  29710  wlkdlem3  29769  wlkdlem4  29770  lfgriswlk  29773  lfgrwlknloop  29774  eulercrct  30330  1to3vfriendship  30369  frgrregorufr0  30412  isgrpo  30586  grpoidinv  30597  grpoideu  30598  grpoidval  30602  grpoidinv2  30604  vcidOLD  30653  vcdi  30654  vcdir  30655  vcass  30656  nvs  30752  nvz  30758  nvtri  30759  mdbr3  32386  mdbr4  32387  mdsl1i  32410  dmdbr6ati  32512  dmdbr7ati  32513  disjunsn  32683  hasheuni  34269  sigaclcu2  34304  prsiga  34315  measvunilem  34396  cntmeas  34410  omssubadd  34484  signsply0  34735  bnj1498  35243  nummin  35274  axprALT2  35290  tz9.1regs  35315  onvf1odlem4  35334  lfuhgr2  35347  cvmsdisj  35498  cvmshmeo  35499  cvmliftlem15  35526  cvmlift2lem12  35542  untangtr  35942  elpotr  36007  dfon2lem7  36015  dfon2lem8  36016  opnrebl2  36549  fnemeet2  36595  fnejoin1  36596  fnejoin2  36597  weiunso  36694  weiunse  36696  weiunwe  36697  dfgcd3  37684  domalom  37766  ctbssinf  37768  nlpfvineqsn  37771  fvineqsnf1  37772  pibt1  37778  pibt2  37779  ptrecube  37987  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimirlem30  38017  poimirlem31  38018  poimirlem32  38019  heicant  38022  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  frinfm  38102  caushft  38128  sstotbnd3  38143  prdstotbnd  38161  heibor1lem  38176  bfplem2  38190  opidonOLD  38219  exidu1  38223  grpomndo  38242  rngoideu  38270  rngodi  38271  rngodir  38272  rngoass  38273  rngoueqz  38307  idladdcl  38386  idllmulcl  38387  idlrmulcl  38388  mpobi123f  38529  iineq12f  38531  mptbi12f  38533  dmqsblocks  39334  pmapglbx  40261  ltrnnid  40628  cdlemefrs32fva  40892  unitscyglem3  42682  fsuppind  43040  dffltz  43084  lerabdioph  43250  ltrabdioph  43253  nerabdioph  43254  dvdsrabdioph  43255  rencldnfi  43266  dford3  43473  pwelg  44004  pwinfi2  44006  ss2iundf  44103  neik0imk0p  44480  gneispace  44578  gneispace0nelrn  44584  ismnushort  44745  ralbidar  44888  rexbidar  44889  ssclaxsep  45426  uniclaxun  45430  uzubico2  46013  climuzlem  46186  xlimxrre  46274  natlocalincr  47321  2reuimp0  47577  bgoldbtbndlem2  48297  bgoldbtbndlem4  48299  mpoexxg2  48829  iuneqconst2  49313  iineqconst2  49314  iunord  50166