Theorem ralimi 3101

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838

This proof depends on definitions:  df-bi 210  df-ral 3079

This theorem is used by:  rexbi  3120  ralrexbid  3121  r19.26  3124  r19.30  3131  2ralimi  3134  3ralimi  3135  4ralimi  3136  5ralimi  3137  6ralimi  3138  r19.21v  3189  rr19.3v  3625  rr19.28v  3626  reu3  3689  uniiunlem  4040  reupick2  4283  uniss2  4906  ss2iun  4974  iineq2  4976  dfiun2g  4993  iunss2  5013  disjss2  5078  disjeq2  5079  triin  5234  replem  5248  zfrep6  5249  reusv2lem5  5372  dmmptg  6242  frpoinsg  6344  fununi  6611  fnmptf  6671  fnmpt  6675  mpteqb  7009  chfnrn  7044  fvn0ssdmfun  7069  dffo5  7099  ffvresb  7121  fmptcof  7126  mpo2eqb  7544  ralrnmpo  7551  abnexg  7753  tfisg  7848  tfis  7849  fun11uni  7928  fiun  7938  f1iun  7939  zfrep6OLD  7950  mpoexxg  8070  el2mpocsbcl  8078  frxp  8120  xpord2indlem  8141  xpord3inddlem  8148  poseq  8152  smores  8337  naddcllem  8660  naddcom  8667  naddrid  8668  naddunif  8678  naddass  8681  riiner  8786  ixpn0  8926  boxriin  8936  unifi2  9300  wemaplem2  9507  frinsg  9721  rankonidlem  9798  acni3  10038  dfac5  10119  dfac12lem2  10135  kmlem6  10146  kmlem8  10148  kmlem13  10153  cfsmolem  10260  fin23lem40  10341  isf32lem2  10344  fin1a2s  10404  hsmexlem2  10417  hsmex3  10424  axcc4  10429  domtriomlem  10432  dcomex  10437  ac6num  10469  iundom  10532  unirnfdomd  10558  konigthlem  10559  iunctb  10565  gch3  10667  wununi  10697  wunpw  10698  wunpr  10700  eltsk2g  10742  tskpwss  10743  tskpw  10744  grupw  10786  gruurn  10789  intgru  10805  grothpw  10817  grothpwex  10818  grothomex  10820  axgroth3  10822  suplem1pr  11043  supexpr  11045  supsr  11103  fimaxre3  12167  xrsupexmnf  13337  xrinfmexpnf  13338  fsuppmapnn0fiublem  14033  fsuppmapnn0fiub  14034  fsuppmapnn0fiubex  14035  mptnn0fsuppd  14041  rexanre  15405  rexuz3  15407  cau3lem  15413  caubnd2  15416  caubnd  15417  rlim0  15566  rlim0lt  15567  climi2  15569  climi0  15570  climrlim2  15605  rlimres  15616  o1rlimmul  15677  caurcvg  15735  caurcvg2  15736  caucvg  15737  caucvgb  15738  sumeq2  15752  prodeq2  15973  ndvdssub  16473  gcdcllem1  16563  coprmproddvdslem  16726  vdwnnlem1  17061  imasaddfnlem  17588  catidex  17736  catlid  17745  catrid  17746  catcocl  17747  catpropd  17771  subcidcl  17907  funcid  17933  setcepi  18151  tsrss  18651  mgmidmo  18724  gsumval2  18750  isnmnd  18802  issubg2  19214  gagrpid  19370  gaass  19373  cygabl  19967  dprdcntz  20086  dprddisj  20087  abveq0  20932  abvmul  20935  abvtri  20936  psgndiflemB  21761  phllmhm  21793  ipcj  21795  ipeq0  21799  mdetmul  22791  pmatcollpw2lem  22945  eltg2b  23127  iincld  23207  iuncld  23213  isclo2  23256  neips  23281  neipeltop  23297  lmcvg  23430  t1t0  23516  hauscmplem  23574  bwth  23578  1stcelcls  23629  ptuni2  23744  pttopon  23764  ptcld  23781  ptcnplem  23789  txtube  23808  txlm  23816  xkococnlem  23827  fbun  24008  isfil2  24024  ptcmplem4  24223  ustssel  24374  isucn2  24446  ucncn  24452  metrest  24692  tngngp  24822  tngngp3  24824  ncvsi  25321  iscau4  25449  cmetcaulem  25458  caussi  25467  volfiniun  25717  iunmbl  25723  voliun  25724  mbfdm  25796  itg2seq  25912  itg2i1fseqle  25924  itg2i1fseq2  25926  iblcnlem  25959  limcresi  26055  limciun  26064  rolle  26160  ulmss  26571  rlimcnp  27141  madebdayim  28092  addsuniflem  28205  oldfib  28581  colinearalg  29271  axpasch  29302  axeuclid  29324  axcontlem2  29326  axcontlem4  29328  axcontlem7  29331  axcontlem8  29332  fusgrregdegfi  29930  0grrgr  29941  rusgr1vtxlem  29948  wlkvtxeledg  29984  wlkdlem3  30043  wlkdlem4  30044  lfgriswlk  30047  lfgrwlknloop  30048  eulercrct  30604  1to3vfriendship  30643  frgrregorufr0  30686  isgrpo  30860  grpoidinv  30871  grpoideu  30872  grpoidval  30876  grpoidinv2  30878  vcidOLD  30927  vcdi  30928  vcdir  30929  vcass  30930  nvs  31026  nvz  31032  nvtri  31033  mdbr3  32660  mdbr4  32661  mdsl1i  32684  dmdbr6ati  32786  dmdbr7ati  32787  disjunsn  32950  hasheuni  34484  sigaclcu2  34519  prsiga  34530  measvunilem  34611  cntmeas  34625  omssubadd  34699  signsply0  34947  bnj1498  35458  nummin  35493  axprALT2  35512  tz9.1regs  35555  onvf1odlem4  35598  lfuhgr2  35619  cvmsdisj  35770  cvmshmeo  35771  cvmliftlem15  35798  cvmlift2lem12  35814  untangtr  36214  elpotr  36279  dfon2lem7  36287  dfon2lem8  36288  nmulprop  36690  opnrebl2  36860  fnemeet2  36906  fnejoin1  36907  fnejoin2  36908  weiunso  37005  weiunse  37007  weiunwe  37008  dfgcd3  37996  domalom  38078  ctbssinf  38080  nlpfvineqsn  38083  fvineqsnf1  38084  pibt1  38090  pibt2  38091  ptrecube  38299  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  poimirlem30  38329  poimirlem31  38330  poimirlem32  38331  heicant  38334  ovoliunnfl  38341  voliunnfl  38343  volsupnfl  38344  frinfm  38414  caushft  38440  sstotbnd3  38455  prdstotbnd  38473  heibor1lem  38488  bfplem2  38502  opidonOLD  38531  exidu1  38535  grpomndo  38554  rngoideu  38582  rngodi  38583  rngodir  38584  rngoass  38585  rngoueqz  38619  idladdcl  38698  idllmulcl  38699  idlrmulcl  38700  mpobi123f  38839  iineq12f  38841  mptbi12f  38843  dmqsblocks  39644  pmapglbx  40571  ltrnnid  40938  cdlemefrs32fva  41202  unitscyglem3  42992  fsuppind  43350  dffltz  43394  lerabdioph  43560  ltrabdioph  43563  nerabdioph  43564  dvdsrabdioph  43565  rencldnfi  43576  dford3  43783  pwelg  44314  pwinfi2  44316  ss2iundf  44413  neik0imk0p  44790  gneispace  44888  gneispace0nelrn  44894  ismnushort  45039  ralbidar  45182  rexbidar  45183  ssclaxsep  45719  uniclaxun  45723  uzubico2  46312  climuzlem  46485  xlimxrre  46573  natlocalincr  47620  2reuimp0  47879  bgoldbtbndlem2  48599  bgoldbtbndlem4  48601  mpoexxg2  49146  iuneqconst2  49629  iineqconst2  49630  iunord  50482