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  3623  rr19.28v  3624  reu3  3687  uniiunlem  4041  reupick2  4285  uniss2  4899  ss2iun  4967  iineq2  4969  dfiun2g  4987  iunss2  5007  disjss2  5070  disjeq2  5071  triin  5223  reusv2lem5  5349  dmmptg  6208  frpoinsg  6309  fununi  6575  fnmptf  6636  fnmpt  6640  mpteqb  6969  chfnrn  7003  fvn0ssdmfun  7028  dffo5  7058  ffvresb  7080  fmptcof  7085  mpo2eqb  7500  ralrnmpo  7507  abnexg  7711  tfisg  7806  tfis  7807  fun11uni  7885  fiun  7897  f1iun  7898  zfrep6  7909  mpoexxg  8029  el2mpocsbcl  8037  frxp  8078  xpord2indlem  8099  xpord3inddlem  8106  poseq  8110  smores  8294  naddcllem  8614  naddcom  8620  naddrid  8621  naddunif  8631  naddass  8634  riiner  8739  ixpn0  8880  boxriin  8890  unifi2  9257  wemaplem2  9464  frinsg  9675  rankonidlem  9752  acni3  9969  dfac5  10051  dfac12lem2  10067  kmlem6  10078  kmlem8  10080  kmlem13  10085  cfsmolem  10192  fin23lem40  10273  isf32lem2  10276  fin1a2s  10336  hsmexlem2  10349  hsmex3  10356  axcc4  10361  domtriomlem  10364  dcomex  10369  ac6num  10401  iundom  10464  unirnfdomd  10490  konigthlem  10491  iunctb  10497  gch3  10599  wununi  10629  wunpw  10630  wunpr  10632  eltsk2g  10674  tskpwss  10675  tskpw  10676  grupw  10718  gruurn  10721  intgru  10737  grothpw  10749  grothpwex  10750  grothomex  10752  axgroth3  10754  suplem1pr  10975  supexpr  10977  supsr  11035  fimaxre3  12100  xrsupexmnf  13232  xrinfmexpnf  13233  fsuppmapnn0fiublem  13925  fsuppmapnn0fiub  13926  fsuppmapnn0fiubex  13927  mptnn0fsuppd  13933  rexanre  15282  rexuz3  15284  cau3lem  15290  caubnd2  15293  caubnd  15294  rlim0  15443  rlim0lt  15444  climi2  15446  climi0  15447  climrlim2  15482  rlimres  15493  o1rlimmul  15554  caurcvg  15612  caurcvg2  15613  caucvg  15614  caucvgb  15615  sumeq2  15629  prodeq2  15847  ndvdssub  16348  gcdcllem1  16438  coprmproddvdslem  16601  vdwnnlem1  16935  imasaddfnlem  17461  catidex  17609  catlid  17618  catrid  17619  catcocl  17620  catpropd  17644  subcidcl  17780  funcid  17806  setcepi  18024  tsrss  18524  mgmidmo  18597  gsumval2  18623  isnmnd  18675  issubg2  19083  gagrpid  19235  gaass  19238  cygabl  19832  dprdcntz  19951  dprddisj  19952  abveq0  20763  abvmul  20766  abvtri  20767  psgndiflemB  21567  phllmhm  21599  ipcj  21601  ipeq0  21605  mdetmul  22579  pmatcollpw2lem  22733  eltg2b  22915  iincld  22995  iuncld  23001  isclo2  23044  neips  23069  neipeltop  23085  lmcvg  23218  t1t0  23304  hauscmplem  23362  bwth  23366  1stcelcls  23417  ptuni2  23532  pttopon  23552  ptcld  23569  ptcnplem  23577  txtube  23596  txlm  23604  xkococnlem  23615  fbun  23796  isfil2  23812  ptcmplem4  24011  ustssel  24162  isucn2  24234  ucncn  24240  metrest  24480  tngngp  24610  tngngp3  24612  ncvsi  25119  iscau4  25247  cmetcaulem  25256  caussi  25265  volfiniun  25516  iunmbl  25522  voliun  25523  mbfdm  25595  itg2seq  25711  itg2i1fseqle  25723  itg2i1fseq2  25725  iblcnlem  25758  limcresi  25854  limciun  25863  rolle  25962  ulmss  26374  rlimcnp  26943  madebdayim  27896  addsuniflem  28009  oldfib  28385  colinearalg  28995  axpasch  29026  axeuclid  29048  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  axcontlem8  29056  fusgrregdegfi  29655  0grrgr  29666  rusgr1vtxlem  29673  wlkvtxeledg  29709  wlkdlem3  29768  wlkdlem4  29769  lfgriswlk  29772  lfgrwlknloop  29773  eulercrct  30329  1to3vfriendship  30368  frgrregorufr0  30411  isgrpo  30584  grpoidinv  30595  grpoideu  30596  grpoidval  30600  grpoidinv2  30602  vcidOLD  30651  vcdi  30652  vcdir  30653  vcass  30654  nvs  30750  nvz  30756  nvtri  30757  mdbr3  32384  mdbr4  32385  mdsl1i  32408  dmdbr6ati  32510  dmdbr7ati  32511  disjunsn  32680  hasheuni  34262  sigaclcu2  34297  prsiga  34308  measvunilem  34389  cntmeas  34403  omssubadd  34477  signsply0  34728  bnj1498  35236  nummin  35268  tz9.1regs  35309  onvf1odlem4  35319  lfuhgr2  35332  cvmsdisj  35483  cvmshmeo  35484  cvmliftlem15  35511  cvmlift2lem12  35527  untangtr  35927  elpotr  35992  dfon2lem7  36000  dfon2lem8  36001  opnrebl2  36534  fnemeet2  36580  fnejoin1  36581  fnejoin2  36582  weiunso  36679  weiunse  36681  weiunwe  36682  dfgcd3  37576  domalom  37656  ctbssinf  37658  nlpfvineqsn  37661  fvineqsnf1  37662  pibt1  37668  pibt2  37669  ptrecube  37868  poimirlem25  37893  poimirlem26  37894  poimirlem27  37895  poimirlem30  37898  poimirlem31  37899  poimirlem32  37900  heicant  37903  ovoliunnfl  37910  voliunnfl  37912  volsupnfl  37913  frinfm  37983  caushft  38009  sstotbnd3  38024  prdstotbnd  38042  heibor1lem  38057  bfplem2  38071  opidonOLD  38100  exidu1  38104  grpomndo  38123  rngoideu  38151  rngodi  38152  rngodir  38153  rngoass  38154  rngoueqz  38188  idladdcl  38267  idllmulcl  38268  idlrmulcl  38269  mpobi123f  38410  iineq12f  38412  mptbi12f  38414  dmqsblocks  39215  pmapglbx  40142  ltrnnid  40509  cdlemefrs32fva  40773  unitscyglem3  42564  fsuppind  42945  dffltz  42989  lerabdioph  43159  ltrabdioph  43162  nerabdioph  43163  dvdsrabdioph  43164  rencldnfi  43175  dford3  43382  pwelg  43913  pwinfi2  43915  ss2iundf  44012  neik0imk0p  44389  gneispace  44487  gneispace0nelrn  44493  ismnushort  44654  ralbidar  44797  rexbidar  44798  ssclaxsep  45335  uniclaxun  45339  uzubico2  45925  climuzlem  46098  xlimxrre  46186  natlocalincr  47231  2reuimp0  47471  bgoldbtbndlem2  48163  bgoldbtbndlem4  48165  mpoexxg2  48695  iuneqconst2  49179  iineqconst2  49180  iunord  50032