Theorem ralimi 3075

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052

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 207  df-ral 3053

This theorem is referenced by:  rexbi  3094  ralrexbid  3095  r19.26  3098  r19.30  3105  2ralimi  3108  3ralimi  3109  4ralimi  3110  5ralimi  3111  6ralimi  3112  r19.21v  3163  rr19.3v  3610  rr19.28v  3611  reu3  3674  uniiunlem  4028  reupick2  4272  uniss2  4885  ss2iun  4953  iineq2  4955  dfiun2g  4973  iunss2  4993  disjss2  5056  disjeq2  5057  triin  5209  replem  5223  zfrep6  5224  reusv2lem5  5339  dmmptg  6200  frpoinsg  6301  fununi  6567  fnmptf  6628  fnmpt  6632  mpteqb  6961  chfnrn  6995  fvn0ssdmfun  7020  dffo5  7050  ffvresb  7072  fmptcof  7077  mpo2eqb  7492  ralrnmpo  7499  abnexg  7703  tfisg  7798  tfis  7799  fun11uni  7877  fiun  7889  f1iun  7890  zfrep6OLD  7901  mpoexxg  8021  el2mpocsbcl  8028  frxp  8069  xpord2indlem  8090  xpord3inddlem  8097  poseq  8101  smores  8285  naddcllem  8605  naddcom  8611  naddrid  8612  naddunif  8622  naddass  8625  riiner  8730  ixpn0  8871  boxriin  8881  unifi2  9248  wemaplem2  9455  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  20786  abvmul  20789  abvtri  20790  psgndiflemB  21590  phllmhm  21622  ipcj  21624  ipeq0  21628  mdetmul  22598  pmatcollpw2lem  22752  eltg2b  22934  iincld  23014  iuncld  23020  isclo2  23063  neips  23088  neipeltop  23104  lmcvg  23237  t1t0  23323  hauscmplem  23381  bwth  23385  1stcelcls  23436  ptuni2  23551  pttopon  23571  ptcld  23588  ptcnplem  23596  txtube  23615  txlm  23623  xkococnlem  23634  fbun  23815  isfil2  23831  ptcmplem4  24030  ustssel  24181  isucn2  24253  ucncn  24259  metrest  24499  tngngp  24629  tngngp3  24631  ncvsi  25128  iscau4  25256  cmetcaulem  25265  caussi  25274  volfiniun  25524  iunmbl  25530  voliun  25531  mbfdm  25603  itg2seq  25719  itg2i1fseqle  25731  itg2i1fseq2  25733  iblcnlem  25766  limcresi  25862  limciun  25871  rolle  25967  ulmss  26375  rlimcnp  26942  madebdayim  27894  addsuniflem  28007  oldfib  28383  colinearalg  28993  axpasch  29024  axeuclid  29046  axcontlem2  29048  axcontlem4  29050  axcontlem7  29053  axcontlem8  29054  fusgrregdegfi  29653  0grrgr  29664  rusgr1vtxlem  29671  wlkvtxeledg  29707  wlkdlem3  29766  wlkdlem4  29767  lfgriswlk  29770  lfgrwlknloop  29771  eulercrct  30327  1to3vfriendship  30366  frgrregorufr0  30409  isgrpo  30583  grpoidinv  30594  grpoideu  30595  grpoidval  30599  grpoidinv2  30601  vcidOLD  30650  vcdi  30651  vcdir  30652  vcass  30653  nvs  30749  nvz  30755  nvtri  30756  mdbr3  32383  mdbr4  32384  mdsl1i  32407  dmdbr6ati  32509  dmdbr7ati  32510  disjunsn  32679  hasheuni  34245  sigaclcu2  34280  prsiga  34291  measvunilem  34372  cntmeas  34386  omssubadd  34460  signsply0  34711  bnj1498  35219  nummin  35252  axprALT2  35269  tz9.1regs  35294  onvf1odlem4  35304  lfuhgr2  35317  cvmsdisj  35468  cvmshmeo  35469  cvmliftlem15  35496  cvmlift2lem12  35512  untangtr  35912  elpotr  35977  dfon2lem7  35985  dfon2lem8  35986  opnrebl2  36519  fnemeet2  36565  fnejoin1  36566  fnejoin2  36567  weiunso  36664  weiunse  36666  weiunwe  36667  dfgcd3  37654  domalom  37734  ctbssinf  37736  nlpfvineqsn  37739  fvineqsnf1  37740  pibt1  37746  pibt2  37747  ptrecube  37955  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  heicant  37990  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  frinfm  38070  caushft  38096  sstotbnd3  38111  prdstotbnd  38129  heibor1lem  38144  bfplem2  38158  opidonOLD  38187  exidu1  38191  grpomndo  38210  rngoideu  38238  rngodi  38239  rngodir  38240  rngoass  38241  rngoueqz  38275  idladdcl  38354  idllmulcl  38355  idlrmulcl  38356  mpobi123f  38497  iineq12f  38499  mptbi12f  38501  dmqsblocks  39302  pmapglbx  40229  ltrnnid  40596  cdlemefrs32fva  40860  unitscyglem3  42650  fsuppind  43037  dffltz  43081  lerabdioph  43251  ltrabdioph  43254  nerabdioph  43255  dvdsrabdioph  43256  rencldnfi  43267  dford3  43474  pwelg  44005  pwinfi2  44007  ss2iundf  44104  neik0imk0p  44481  gneispace  44579  gneispace0nelrn  44585  ismnushort  44746  ralbidar  44889  rexbidar  44890  ssclaxsep  45427  uniclaxun  45431  uzubico2  46016  climuzlem  46189  xlimxrre  46277  natlocalincr  47322  2reuimp0  47574  bgoldbtbndlem2  48294  bgoldbtbndlem4  48296  mpoexxg2  48826  iuneqconst2  49310  iineqconst2  49311  iunord  50163