Theorem ralimi 3069

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

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

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

This theorem depends on definitions:  df-bi 207  df-ral 3048

This theorem is referenced by:  rexbi  3088  ralrexbid  3089  r19.26  3092  r19.30  3099  2ralimi  3102  3ralimi  3103  4ralimi  3104  5ralimi  3105  6ralimi  3106  r19.21v  3157  rr19.3v  3617  rr19.28v  3618  reu3  3681  uniiunlem  4032  reupick2  4276  ralf0  4459  uniss2  4887  ss2iun  4955  iineq2  4957  dfiun2g  4975  iunss2  4993  disjss2  5056  disjeq2  5057  triin  5209  reusv2lem5  5335  dmmptg  6184  frpoinsg  6285  fununi  6551  fnmptf  6612  fnmpt  6616  mpteqb  6943  chfnrn  6977  fvn0ssdmfun  7002  dffo5  7032  ffvresb  7053  fmptcof  7058  mpo2eqb  7473  ralrnmpo  7480  abnexg  7684  tfisg  7779  tfis  7780  fun11uni  7858  fiun  7870  f1iun  7871  zfrep6  7882  mpoexxg  8002  el2mpocsbcl  8010  frxp  8051  xpord2indlem  8072  xpord3inddlem  8079  poseq  8083  smores  8267  naddcllem  8586  naddcom  8592  naddrid  8593  naddunif  8603  naddass  8606  riiner  8709  ixpn0  8849  boxriin  8859  unifi2  9224  wemaplem2  9428  frinsg  9639  rankonidlem  9716  acni3  9933  dfac5  10015  dfac12lem2  10031  kmlem6  10042  kmlem8  10044  kmlem13  10049  cfsmolem  10156  fin23lem40  10237  isf32lem2  10240  fin1a2s  10300  hsmexlem2  10313  hsmex3  10320  axcc4  10325  domtriomlem  10328  dcomex  10333  ac6num  10365  iundom  10428  unirnfdomd  10453  konigthlem  10454  iunctb  10460  gch3  10562  wununi  10592  wunpw  10593  wunpr  10595  eltsk2g  10637  tskpwss  10638  tskpw  10639  grupw  10681  gruurn  10684  intgru  10700  grothpw  10712  grothpwex  10713  grothomex  10715  axgroth3  10717  suplem1pr  10938  supexpr  10940  supsr  10998  fimaxre3  12063  xrsupexmnf  13199  xrinfmexpnf  13200  fsuppmapnn0fiublem  13892  fsuppmapnn0fiub  13893  fsuppmapnn0fiubex  13894  mptnn0fsuppd  13900  rexanre  15249  rexuz3  15251  cau3lem  15257  caubnd2  15260  caubnd  15261  rlim0  15410  rlim0lt  15411  climi2  15413  climi0  15414  climrlim2  15449  rlimres  15460  o1rlimmul  15521  caurcvg  15579  caurcvg2  15580  caucvg  15581  caucvgb  15582  sumeq2  15596  prodeq2  15814  ndvdssub  16315  gcdcllem1  16405  coprmproddvdslem  16568  vdwnnlem1  16902  imasaddfnlem  17427  catidex  17575  catlid  17584  catrid  17585  catcocl  17586  catpropd  17610  subcidcl  17746  funcid  17772  setcepi  17990  tsrss  18490  mgmidmo  18563  gsumval2  18589  isnmnd  18641  issubg2  19049  gagrpid  19201  gaass  19204  cygabl  19798  dprdcntz  19917  dprddisj  19918  abveq0  20728  abvmul  20731  abvtri  20732  psgndiflemB  21532  phllmhm  21564  ipcj  21566  ipeq0  21570  mdetmul  22533  pmatcollpw2lem  22687  eltg2b  22869  iincld  22949  iuncld  22955  isclo2  22998  neips  23023  neipeltop  23039  lmcvg  23172  t1t0  23258  hauscmplem  23316  bwth  23320  1stcelcls  23371  ptuni2  23486  pttopon  23506  ptcld  23523  ptcnplem  23531  txtube  23550  txlm  23558  xkococnlem  23569  fbun  23750  isfil2  23766  ptcmplem4  23965  ustssel  24116  isucn2  24188  ucncn  24194  metrest  24434  tngngp  24564  tngngp3  24566  ncvsi  25073  iscau4  25201  cmetcaulem  25210  caussi  25219  volfiniun  25470  iunmbl  25476  voliun  25477  mbfdm  25549  itg2seq  25665  itg2i1fseqle  25677  itg2i1fseq2  25679  iblcnlem  25712  limcresi  25808  limciun  25817  rolle  25916  ulmss  26328  rlimcnp  26897  madebdayim  27828  addsuniflem  27939  colinearalg  28883  axpasch  28914  axeuclid  28936  axcontlem2  28938  axcontlem4  28940  axcontlem7  28943  axcontlem8  28944  fusgrregdegfi  29543  0grrgr  29554  rusgr1vtxlem  29561  wlkvtxeledg  29597  wlkdlem3  29656  wlkdlem4  29657  lfgriswlk  29660  lfgrwlknloop  29661  eulercrct  30214  1to3vfriendship  30253  frgrregorufr0  30296  isgrpo  30469  grpoidinv  30480  grpoideu  30481  grpoidval  30485  grpoidinv2  30487  vcidOLD  30536  vcdi  30537  vcdir  30538  vcass  30539  nvs  30635  nvz  30641  nvtri  30642  mdbr3  32269  mdbr4  32270  mdsl1i  32293  dmdbr6ati  32395  dmdbr7ati  32396  disjunsn  32566  hasheuni  34090  sigaclcu2  34125  prsiga  34136  measvunilem  34217  cntmeas  34231  omssubadd  34305  signsply0  34556  bnj1498  35065  nummin  35096  tz9.1regs  35122  onvf1odlem4  35142  lfuhgr2  35155  cvmsdisj  35306  cvmshmeo  35307  cvmliftlem15  35334  cvmlift2lem12  35350  untangtr  35750  elpotr  35815  dfon2lem7  35823  dfon2lem8  35824  opnrebl2  36355  fnemeet2  36401  fnejoin1  36402  fnejoin2  36403  weiunso  36500  weiunse  36502  weiunwe  36503  dfgcd3  37358  domalom  37438  ctbssinf  37440  nlpfvineqsn  37443  fvineqsnf1  37444  pibt1  37450  pibt2  37451  ptrecube  37660  poimirlem25  37685  poimirlem26  37686  poimirlem27  37687  poimirlem30  37690  poimirlem31  37691  poimirlem32  37692  heicant  37695  ovoliunnfl  37702  voliunnfl  37704  volsupnfl  37705  frinfm  37775  caushft  37801  sstotbnd3  37816  prdstotbnd  37834  heibor1lem  37849  bfplem2  37863  opidonOLD  37892  exidu1  37896  grpomndo  37915  rngoideu  37943  rngodi  37944  rngodir  37945  rngoass  37946  rngoueqz  37980  idladdcl  38059  idllmulcl  38060  idlrmulcl  38061  mpobi123f  38202  iineq12f  38204  mptbi12f  38206  dmqsblocks  38891  pmapglbx  39808  ltrnnid  40175  cdlemefrs32fva  40439  unitscyglem3  42230  fsuppind  42623  dffltz  42667  lerabdioph  42838  ltrabdioph  42841  nerabdioph  42842  dvdsrabdioph  42843  rencldnfi  42854  dford3  43061  pwelg  43593  pwinfi2  43595  ss2iundf  43692  neik0imk0p  44069  gneispace  44167  gneispace0nelrn  44173  ismnushort  44334  ralbidar  44477  rexbidar  44478  ssclaxsep  45015  uniclaxun  45019  uzubico2  45608  climuzlem  45781  xlimxrre  45869  natlocalincr  46914  2reuimp0  47145  bgoldbtbndlem2  47837  bgoldbtbndlem4  47839  mpoexxg2  48369  iuneqconst2  48854  iineqconst2  48855  iunord  49708