Theorem ralimi 3102

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∀wral 3079

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

This theorem depends on definitions:  df-bi 210  df-ral 3080

This theorem is referenced by:  rexbi  3121  ralrexbid  3122  r19.26  3125  r19.30  3132  2ralimi  3135  3ralimi  3136  4ralimi  3137  5ralimi  3138  6ralimi  3139  r19.21v  3190  rr19.3v  3627  rr19.28v  3628  reu3  3691  uniiunlem  4042  reupick2  4285  uniss2  4908  ss2iun  4976  iineq2  4978  dfiun2g  4995  iunss2  5015  disjss2  5080  disjeq2  5081  triin  5236  replem  5250  zfrep6  5251  reusv2lem5  5375  dmmptg  6245  frpoinsg  6346  fununi  6613  fnmptf  6673  fnmpt  6677  mpteqb  7011  chfnrn  7046  fvn0ssdmfun  7071  dffo5  7101  ffvresb  7123  fmptcof  7128  mpo2eqb  7544  ralrnmpo  7551  abnexg  7756  tfisg  7851  tfis  7852  fun11uni  7931  fiun  7941  f1iun  7942  zfrep6OLD  7953  mpoexxg  8073  el2mpocsbcl  8081  frxp  8123  xpord2indlem  8144  xpord3inddlem  8151  poseq  8155  smores  8340  naddcllem  8663  naddcom  8670  naddrid  8671  naddunif  8681  naddass  8684  riiner  8789  ixpn0  8929  boxriin  8939  unifi2  9303  wemaplem2  9510  frinsg  9724  rankonidlem  9801  acni3  10032  dfac5  10113  dfac12lem2  10129  kmlem6  10140  kmlem8  10142  kmlem13  10147  cfsmolem  10255  fin23lem40  10336  isf32lem2  10339  fin1a2s  10399  hsmexlem2  10412  hsmex3  10419  axcc4  10424  domtriomlem  10427  dcomex  10432  ac6num  10464  iundom  10527  unirnfdomd  10553  konigthlem  10554  iunctb  10560  gch3  10662  wununi  10692  wunpw  10693  wunpr  10695  eltsk2g  10737  tskpwss  10738  tskpw  10739  grupw  10781  gruurn  10784  intgru  10800  grothpw  10812  grothpwex  10813  grothomex  10815  axgroth3  10817  suplem1pr  11038  supexpr  11040  supsr  11098  fimaxre3  12162  xrsupexmnf  13332  xrinfmexpnf  13333  fsuppmapnn0fiublem  14028  fsuppmapnn0fiub  14029  fsuppmapnn0fiubex  14030  mptnn0fsuppd  14036  rexanre  15400  rexuz3  15402  cau3lem  15408  caubnd2  15411  caubnd  15412  rlim0  15561  rlim0lt  15562  climi2  15564  climi0  15565  climrlim2  15600  rlimres  15611  o1rlimmul  15672  caurcvg  15730  caurcvg2  15731  caucvg  15732  caucvgb  15733  sumeq2  15747  prodeq2  15968  ndvdssub  16468  gcdcllem1  16558  coprmproddvdslem  16721  vdwnnlem1  17056  imasaddfnlem  17583  catidex  17731  catlid  17740  catrid  17741  catcocl  17742  catpropd  17766  subcidcl  17902  funcid  17928  setcepi  18146  tsrss  18646  mgmidmo  18719  gsumval2  18745  isnmnd  18797  issubg2  19209  gagrpid  19365  gaass  19368  cygabl  19962  dprdcntz  20081  dprddisj  20082  abveq0  20902  abvmul  20905  abvtri  20906  psgndiflemB  21731  phllmhm  21763  ipcj  21765  ipeq0  21769  mdetmul  22761  pmatcollpw2lem  22915  eltg2b  23097  iincld  23177  iuncld  23183  isclo2  23226  neips  23251  neipeltop  23267  lmcvg  23400  t1t0  23486  hauscmplem  23544  bwth  23548  1stcelcls  23599  ptuni2  23714  pttopon  23734  ptcld  23751  ptcnplem  23759  txtube  23778  txlm  23786  xkococnlem  23797  fbun  23978  isfil2  23994  ptcmplem4  24193  ustssel  24344  isucn2  24416  ucncn  24422  metrest  24662  tngngp  24792  tngngp3  24794  ncvsi  25291  iscau4  25419  cmetcaulem  25428  caussi  25437  volfiniun  25687  iunmbl  25693  voliun  25694  mbfdm  25766  itg2seq  25882  itg2i1fseqle  25894  itg2i1fseq2  25896  iblcnlem  25929  limcresi  26025  limciun  26034  rolle  26130  ulmss  26541  rlimcnp  27111  madebdayim  28062  addsuniflem  28175  oldfib  28551  colinearalg  29241  axpasch  29272  axeuclid  29294  axcontlem2  29296  axcontlem4  29298  axcontlem7  29301  axcontlem8  29302  fusgrregdegfi  29900  0grrgr  29911  rusgr1vtxlem  29918  wlkvtxeledg  29954  wlkdlem3  30013  wlkdlem4  30014  lfgriswlk  30017  lfgrwlknloop  30018  eulercrct  30574  1to3vfriendship  30613  frgrregorufr0  30656  isgrpo  30830  grpoidinv  30841  grpoideu  30842  grpoidval  30846  grpoidinv2  30848  vcidOLD  30897  vcdi  30898  vcdir  30899  vcass  30900  nvs  30996  nvz  31002  nvtri  31003  mdbr3  32630  mdbr4  32631  mdsl1i  32654  dmdbr6ati  32756  dmdbr7ati  32757  disjunsn  32920  hasheuni  34456  sigaclcu2  34491  prsiga  34502  measvunilem  34583  cntmeas  34597  omssubadd  34671  signsply0  34919  bnj1498  35430  nummin  35465  axprALT2  35484  tz9.1regs  35528  onvf1odlem4  35571  lfuhgr2  35592  cvmsdisj  35743  cvmshmeo  35744  cvmliftlem15  35771  cvmlift2lem12  35787  untangtr  36187  elpotr  36252  dfon2lem7  36260  dfon2lem8  36261  nmulprop  36663  opnrebl2  36813  fnemeet2  36859  fnejoin1  36860  fnejoin2  36861  weiunso  36958  weiunse  36960  weiunwe  36961  dfgcd3  37949  domalom  38031  ctbssinf  38033  nlpfvineqsn  38036  fvineqsnf1  38037  pibt1  38043  pibt2  38044  ptrecube  38252  poimirlem25  38277  poimirlem26  38278  poimirlem27  38279  poimirlem30  38282  poimirlem31  38283  poimirlem32  38284  heicant  38287  ovoliunnfl  38294  voliunnfl  38296  volsupnfl  38297  frinfm  38367  caushft  38393  sstotbnd3  38408  prdstotbnd  38426  heibor1lem  38441  bfplem2  38455  opidonOLD  38484  exidu1  38488  grpomndo  38507  rngoideu  38535  rngodi  38536  rngodir  38537  rngoass  38538  rngoueqz  38572  idladdcl  38651  idllmulcl  38652  idlrmulcl  38653  mpobi123f  38792  iineq12f  38794  mptbi12f  38796  dmqsblocks  39597  pmapglbx  40524  ltrnnid  40891  cdlemefrs32fva  41155  unitscyglem3  42945  fsuppind  43305  dffltz  43349  lerabdioph  43515  ltrabdioph  43518  nerabdioph  43519  dvdsrabdioph  43520  rencldnfi  43531  dford3  43738  pwelg  44269  pwinfi2  44271  ss2iundf  44368  neik0imk0p  44745  gneispace  44843  gneispace0nelrn  44849  ismnushort  44994  ralbidar  45137  rexbidar  45138  ssclaxsep  45674  uniclaxun  45678  uzubico2  46267  climuzlem  46440  xlimxrre  46528  natlocalincr  47575  2reuimp0  47834  bgoldbtbndlem2  48554  bgoldbtbndlem4  48556  mpoexxg2  49101  iuneqconst2  49584  iineqconst2  49585  iunord  50437