Theorem ralimi 3128

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3106

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 210  df-ral 3111

This theorem is referenced by:  2ralimi  3129  r19.26  3137  r19.29  3216  r19.30  3293  r19.35  3295  rr19.3v  3607  rr19.28v  3608  reu3  3666  uniiunlem  4012  reupick2  4241  uniss2  4833  ss2iun  4899  iineq2  4901  iunss2  4936  disjss2  4998  disjeq2  4999  triin  5151  reusv2lem5  5268  dmmptg  6063  wfisg  6151  fununi  6399  fnmptf  6456  fnmpt  6460  mpteqb  6764  chfnrn  6796  fvn0ssdmfun  6819  dffo5  6847  ffvresb  6865  fmptcof  6869  mpo2eqb  7262  ralrnmpo  7268  abnexg  7458  tfis  7549  fun11uni  7619  fiun  7626  f1iun  7627  zfrep6  7638  mpoexxg  7756  el2mpocsbcl  7763  frxp  7803  smores  7972  riiner  8353  ixpn0  8477  boxriin  8487  unifi2  8798  wemaplem2  8995  rankonidlem  9241  acni3  9458  dfac5  9539  dfac12lem2  9555  kmlem6  9566  kmlem8  9568  kmlem13  9573  cfsmolem  9681  fin23lem40  9762  isf32lem2  9765  fin1a2s  9825  hsmexlem2  9838  hsmex3  9845  axcc4  9850  domtriomlem  9853  dcomex  9858  ac6num  9890  iundom  9953  unirnfdomd  9978  konigthlem  9979  iunctb  9985  gch3  10087  wununi  10117  wunpw  10118  wunpr  10120  eltsk2g  10162  tskpwss  10163  tskpw  10164  grupw  10206  gruurn  10209  intgru  10225  grothpw  10237  grothpwex  10238  grothomex  10240  axgroth3  10242  suplem1pr  10463  supexpr  10465  supsr  10523  fimaxre3  11575  xrsupexmnf  12686  xrinfmexpnf  12687  fsuppmapnn0fiublem  13353  fsuppmapnn0fiub  13354  fsuppmapnn0fiubex  13355  mptnn0fsuppd  13361  rexanre  14698  rexuz3  14700  cau3lem  14706  caubnd2  14709  caubnd  14710  rlim0  14857  rlim0lt  14858  climi2  14860  climi0  14861  climrlim2  14896  rlimres  14907  o1rlimmul  14967  caurcvg  15025  caurcvg2  15026  caucvg  15027  caucvgb  15028  sumeq2  15043  prodeq2  15260  ndvdssub  15750  gcdcllem1  15838  coprmproddvdslem  15996  vdwnnlem1  16321  imasaddfnlem  16793  catidex  16937  catlid  16946  catrid  16947  catcocl  16948  catpropd  16971  subcidcl  17106  funcid  17132  setcepi  17340  tsrss  17825  mgmidmo  17862  gsumval2  17888  isnmnd  17907  issubg2  18286  gagrpid  18416  gaass  18419  cygabl  19003  dprdcntz  19123  dprddisj  19124  abveq0  19590  abvmul  19593  abvtri  19594  psgndiflemB  20289  phllmhm  20321  ipcj  20323  ipeq0  20327  mdetmul  21228  pmatcollpw2lem  21382  eltg2b  21564  iincld  21644  iuncld  21650  isclo2  21693  neips  21718  neipeltop  21734  lmcvg  21867  t1t0  21953  hauscmplem  22011  bwth  22015  1stcelcls  22066  ptuni2  22181  pttopon  22201  ptcld  22218  ptcnplem  22226  txtube  22245  txlm  22253  xkococnlem  22264  fbun  22445  isfil2  22461  ptcmplem4  22660  ustssel  22811  isucn2  22885  ucncn  22891  metrest  23131  tngngp  23260  tngngp3  23262  ncvsi  23756  iscau4  23883  cmetcaulem  23892  caussi  23901  volfiniun  24151  iunmbl  24157  voliun  24158  mbfdm  24230  itg2seq  24346  itg2i1fseqle  24358  itg2i1fseq2  24360  iblcnlem  24392  limcresi  24488  limciun  24497  rolle  24593  ulmss  24992  rlimcnp  25551  colinearalg  26704  axpasch  26735  axeuclid  26757  axcontlem2  26759  axcontlem4  26761  axcontlem7  26764  axcontlem8  26765  fusgrregdegfi  27359  0grrgr  27370  rusgr1vtxlem  27377  wlkvtxeledg  27413  wlkdlem3  27474  wlkdlem4  27475  lfgriswlk  27478  lfgrwlknloop  27479  eulercrct  28027  1to3vfriendship  28066  frgrregorufr0  28109  isgrpo  28280  grpoidinv  28291  grpoideu  28292  grpoidval  28296  grpoidinv2  28298  vcidOLD  28347  vcdi  28348  vcdir  28349  vcass  28350  nvs  28446  nvz  28452  nvtri  28453  mdbr3  30080  mdbr4  30081  mdsl1i  30104  dmdbr6ati  30206  dmdbr7ati  30207  disjunsn  30357  hasheuni  31454  sigaclcu2  31489  prsiga  31500  measvunilem  31581  cntmeas  31595  omssubadd  31668  signsply0  31931  bnj1498  32443  nummin  32474  lfuhgr2  32478  cvmsdisj  32630  cvmshmeo  32631  cvmliftlem15  32658  cvmlift2lem12  32674  untangtr  33053  elpotr  33139  dfon2lem7  33147  dfon2lem8  33148  tfisg  33168  frpoinsg  33194  frinsg  33200  poseq  33208  opnrebl2  33782  fnemeet2  33828  fnejoin1  33829  fnejoin2  33830  dfgcd3  34738  domalom  34821  ctbssinf  34823  nlpfvineqsn  34826  fvineqsnf1  34827  pibt1  34833  pibt2  34834  ptrecube  35057  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  heicant  35092  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  frinfm  35173  caushft  35199  sstotbnd3  35214  prdstotbnd  35232  heibor1lem  35247  bfplem2  35261  opidonOLD  35290  exidu1  35294  grpomndo  35313  rngoideu  35341  rngodi  35342  rngodir  35343  rngoass  35344  rngoueqz  35378  idladdcl  35457  idllmulcl  35458  idlrmulcl  35459  mpobi123f  35600  iineq12f  35602  mptbi12f  35604  pmapglbx  37065  ltrnnid  37432  cdlemefrs32fva  37696  fsuppind  39456  dffltz  39615  lerabdioph  39746  ltrabdioph  39749  nerabdioph  39750  dvdsrabdioph  39751  rencldnfi  39762  dford3  39969  pwelg  40259  pwinfi2  40261  ss2iundf  40360  neik0imk0p  40739  gneispace  40837  gneispace0nelrn  40843  ralbidar  41149  rexbidar  41150  uzubico2  42207  climuzlem  42385  xlimxrre  42473  2reuimp0  43670  bgoldbtbndlem2  44324  bgoldbtbndlem4  44326  mpoexxg2  44739  iunord  45206