Theorem ralimi 3103

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∀wral 3080

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

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

This theorem is used by:  rexbi  3122  ralrexbid  3123  r19.26  3126  r19.30  3133  2ralimi  3136  3ralimi  3137  4ralimi  3138  5ralimi  3139  6ralimi  3140  r19.21v  3191  rr19.3v  3624  rr19.28v  3625  reu3  3688  uniiunlem  4015  reupick2  4279  uniss2  4907  ss2iun  4975  iineq2  4977  dfiun2g  4993  iunss2  5013  disjss2  5078  disjeq2  5079  triin  5235  replem  5247  zfrep6  5248  reusv2lem5  5371  dmmptg  6262  frinf  6316  frpoinsg  6372  fununi  6645  fnmptf  6705  fnmpt  6709  mpteqb  7044  chfnrn  7079  fvn0ssdmfun  7106  dffo5  7136  ffvresb  7158  fmptcof  7163  mpo2eqb  7583  ralrnmpo  7591  abnexg  7802  tfisg  7899  tfis  7900  fun11uni  7979  fiun  7989  f1iun  7990  zfrep6OLD  8001  mpoexxg  8123  el2mpocsbcl  8131  frxp  8175  xpord2indlem  8201  xpord3inddlem  8208  poseq  8212  smores  8398  naddcllem  8723  naddcom  8730  naddrid  8731  naddunif  8741  naddass  8744  riiner  8849  ixpn0  8996  boxriin  9006  unifi2  9372  wemaplem2  9578  frinsg  9792  rankonidlem  9875  acni3  10165  dfac5  10246  dfac12lem2  10262  kmlem6  10273  kmlem8  10275  kmlem13  10280  cfsmolem  10387  fin23lem40  10468  isf32lem2  10471  fin1a2s  10531  hsmexlem2  10544  hsmex3  10551  axcc4  10556  domtriomlem  10559  dcomex  10564  ac6num  10596  iundom  10665  unirnfdomd  10691  konigthlem  10692  iunctb  10698  gch3  10800  wununi  10830  wunpw  10831  wunpr  10833  eltsk2g  10875  tskpwss  10876  tskpw  10877  grupw  10919  gruurn  10922  intgru  10938  grothpw  10950  grothpwex  10951  grothomex  10953  axgroth3  10955  suplem1pr  11176  supexpr  11178  supsr  11236  fimaxre3  12303  xrsupexmnf  13475  xrinfmexpnf  13476  fsuppmapnn0fiublem  14173  fsuppmapnn0fiub  14174  fsuppmapnn0fiubex  14175  mptnn0fsuppd  14181  rexanre  15558  rexuz3  15560  cau3lem  15566  caubnd2  15569  caubnd  15570  rlim0  15719  rlim0lt  15720  climi2  15722  climi0  15723  climrlim2  15758  rlimres  15769  o1rlimmul  15830  caurcvg  15888  caurcvg2  15889  caucvg  15890  caucvgb  15891  sumeq2  15905  prodeq2  16125  ndvdssub  16623  gcdcllem1  16713  coprmproddvdslem  16881  vdwnnlem1  17217  imasaddfnlem  17750  catidex  17898  catlid  17907  catrid  17908  catcocl  17909  catpropd  17933  subcidcl  18069  funcid  18095  setcepi  18313  tsrss  18813  mgmidmo  18888  mgmidpfod  18907  gsumval2  18925  isnmnd  18977  issubg2  19402  gagrpid  19559  gaass  19562  cygabl  20156  dprdcntz  20275  dprddisj  20276  abveq0  21126  abvmul  21129  abvtri  21130  psgndiflemB  21961  phllmhm  21993  ipcj  21995  ipeq0  21999  mdetmul  22993  pmatcollpw2lem  23150  eltg2b  23332  iincld  23412  iuncld  23418  isclo2  23461  neips  23486  neipeltop  23502  lmcvg  23635  t1t0  23721  hauscmplem  23779  bwth  23783  1stcelcls  23835  ptuni2  23950  pttopon  23970  ptcld  23987  ptcnplem  23995  txtube  24014  txlm  24022  xkococnlem  24033  fbun  24214  isfil2  24230  ptcmplem4  24429  ustssel  24580  isucn2  24652  ucncn  24658  metrest  24898  tngngp  25028  tngngp3  25030  ncvsi  25527  iscau4  25655  cmetcaulem  25664  caussi  25673  volfiniun  25923  iunmbl  25929  voliun  25930  mbfdm  26002  itg2seq  26118  itg2i1fseqle  26130  itg2i1fseq2  26132  iblcnlem  26164  limcresi  26260  limciun  26269  rolle  26365  ulmss  26781  rlimcnp  27350  madebdayim  28331  addsuniflem  28444  oldfib  28820  colinearalg  29545  axpasch  29576  axeuclid  29598  axcontlem2  29600  axcontlem4  29602  axcontlem7  29605  axcontlem8  29606  lfuhgr2  29784  fusgrregdegfi  30207  0grrgr  30218  rusgr1vtxlem  30225  wlkvtxeledg  30261  wlkdlem3  30320  wlkdlem4  30321  lfgriswlk  30328  lfgrwlknloop  30329  eulercrct  30900  1to3vfriendship  30939  frgrregorufr0  30982  isgrpo  31156  grpoidinv  31167  grpoideu  31168  grpoidval  31172  grpoidinv2  31174  vcidOLD  31223  vcdi  31224  vcdir  31225  vcass  31226  nvs  31322  nvz  31328  nvtri  31329  mdbr3  32956  mdbr4  32957  mdsl1i  32980  dmdbr6ati  33082  dmdbr7ati  33083  disjunsn  33286  hasheuni  34828  sigaclcu2  34863  prsiga  34874  measvunilem  34956  cntmeas  34970  omssubadd  35043  signsply0  35291  bnj1498  35802  rmo6  35821  nummin  35847  axprALT2  35857  tz9.1regs  35943  onvf1odlem4  36075  srepdflem1  36126  srepdflem2  36127  cvmsdisj  36243  cvmshmeo  36244  cvmliftlem15  36271  cvmlift2lem12  36287  untangtr  36694  elpotr  36758  dfon2lem7  36766  dfon2lem8  36767  nmulprop  37154  opnrebl2  37324  fnemeet2  37370  fnejoin1  37371  fnejoin2  37372  weiunso  37469  weiunse  37471  weiunwe  37472  dfgcd3  38513  domalom  38595  ctbssinf  38597  nlpfvineqsn  38600  fvineqsnf1  38601  pibt1  38607  pibt2  38608  ptrecube  38806  poimirlem25  38831  poimirlem26  38832  poimirlem27  38833  poimirlem30  38836  poimirlem31  38837  poimirlem32  38838  heicant  38841  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  caushft  38961  sstotbnd3  38976  prdstotbnd  38994  heibor1lem  39009  bfplem2  39023  opidonOLD  39052  exidu1  39056  grpomndo  39075  rngoideu  39103  rngodi  39104  rngodir  39105  rngoass  39106  rngoueqz  39140  idladdcl  39219  idllmulcl  39220  idlrmulcl  39221  mpobi123f  39360  iineq12f  39362  mptbi12f  39364  dmqsblocks  40165  pmapglbx  41092  ltrnnid  41459  cdlemefrs32fva  41723  unitscyglem3  43513  fsuppind  43884  dffltz  43936  lerabdioph  44078  ltrabdioph  44081  nerabdioph  44082  dvdsrabdioph  44083  rencldnfi  44094  dford3  44301  pwelg  44822  pwinfi2  44824  ss2iundf  44920  neik0imk0p  45297  gneispace  45395  gneispace0nelrn  45401  ismnushort  45546  ralbidar  45688  rexbidar  45689  ssclaxsep  46236  uniclaxun  46240  uzubico2  46853  climuzlem  47026  xlimxrre  47114  2reuimp0  48458  bgoldbtbndlem2  49177  bgoldbtbndlem4  49179  mpoexxg2  49781  iuneqconst2  50265  iineqconst2  50266  iunord  51190