Theorem ralimi 3089

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∀wral 3066

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

This theorem depends on definitions:  df-bi 206  df-ral 3071

This theorem is referenced by:  2ralimi  3090  r19.26  3097  rexbi  3172  r19.29  3186  ralrexbid  3253  r19.30  3268  r19.30OLD  3269  r19.35  3271  rr19.3v  3600  rr19.28v  3601  reu3  3666  uniiunlem  4024  reupick2  4260  ralf0  4450  uniss2  4880  ss2iun  4948  iineq2  4950  iunss2  4984  disjss2  5047  disjeq2  5048  triin  5211  reusv2lem5  5329  dmmptg  6144  frpoinsg  6245  wfisgOLD  6256  fununi  6507  fnmptf  6567  fnmpt  6571  mpteqb  6891  chfnrn  6923  fvn0ssdmfun  6949  dffo5  6977  ffvresb  6995  fmptcof  6999  mpo2eqb  7400  ralrnmpo  7406  abnexg  7600  tfis  7695  fun11uni  7773  fiun  7779  f1iun  7780  zfrep6  7791  mpoexxg  7909  el2mpocsbcl  7916  frxp  7958  smores  8174  riiner  8562  ixpn0  8701  boxriin  8711  unifi2  9087  wemaplem2  9284  frinsg  9510  rankonidlem  9587  acni3  9804  dfac5  9885  dfac12lem2  9901  kmlem6  9912  kmlem8  9914  kmlem13  9919  cfsmolem  10027  fin23lem40  10108  isf32lem2  10111  fin1a2s  10171  hsmexlem2  10184  hsmex3  10191  axcc4  10196  domtriomlem  10199  dcomex  10204  ac6num  10236  iundom  10299  unirnfdomd  10324  konigthlem  10325  iunctb  10331  gch3  10433  wununi  10463  wunpw  10464  wunpr  10466  eltsk2g  10508  tskpwss  10509  tskpw  10510  grupw  10552  gruurn  10555  intgru  10571  grothpw  10583  grothpwex  10584  grothomex  10586  axgroth3  10588  suplem1pr  10809  supexpr  10811  supsr  10869  fimaxre3  11921  xrsupexmnf  13038  xrinfmexpnf  13039  fsuppmapnn0fiublem  13708  fsuppmapnn0fiub  13709  fsuppmapnn0fiubex  13710  mptnn0fsuppd  13716  rexanre  15056  rexuz3  15058  cau3lem  15064  caubnd2  15067  caubnd  15068  rlim0  15215  rlim0lt  15216  climi2  15218  climi0  15219  climrlim2  15254  rlimres  15265  o1rlimmul  15326  caurcvg  15386  caurcvg2  15387  caucvg  15388  caucvgb  15389  sumeq2  15404  prodeq2  15622  ndvdssub  16116  gcdcllem1  16204  coprmproddvdslem  16365  vdwnnlem1  16694  imasaddfnlem  17237  catidex  17381  catlid  17390  catrid  17391  catcocl  17392  catpropd  17416  subcidcl  17557  funcid  17583  setcepi  17801  tsrss  18305  mgmidmo  18342  gsumval2  18368  isnmnd  18387  issubg2  18768  gagrpid  18898  gaass  18901  cygabl  19489  dprdcntz  19609  dprddisj  19610  abveq0  20084  abvmul  20087  abvtri  20088  psgndiflemB  20803  phllmhm  20835  ipcj  20837  ipeq0  20841  mdetmul  21770  pmatcollpw2lem  21924  eltg2b  22107  iincld  22188  iuncld  22194  isclo2  22237  neips  22262  neipeltop  22278  lmcvg  22411  t1t0  22497  hauscmplem  22555  bwth  22559  1stcelcls  22610  ptuni2  22725  pttopon  22745  ptcld  22762  ptcnplem  22770  txtube  22789  txlm  22797  xkococnlem  22808  fbun  22989  isfil2  23005  ptcmplem4  23204  ustssel  23355  isucn2  23429  ucncn  23435  metrest  23678  tngngp  23816  tngngp3  23818  ncvsi  24313  iscau4  24441  cmetcaulem  24450  caussi  24459  volfiniun  24709  iunmbl  24715  voliun  24716  mbfdm  24788  itg2seq  24905  itg2i1fseqle  24917  itg2i1fseq2  24919  iblcnlem  24951  limcresi  25047  limciun  25056  rolle  25152  ulmss  25554  rlimcnp  26113  colinearalg  27276  axpasch  27307  axeuclid  27329  axcontlem2  27331  axcontlem4  27333  axcontlem7  27336  axcontlem8  27337  fusgrregdegfi  27934  0grrgr  27945  rusgr1vtxlem  27952  wlkvtxeledg  27988  wlkdlem3  28049  wlkdlem4  28050  lfgriswlk  28053  lfgrwlknloop  28054  eulercrct  28602  1to3vfriendship  28641  frgrregorufr0  28684  isgrpo  28855  grpoidinv  28866  grpoideu  28867  grpoidval  28871  grpoidinv2  28873  vcidOLD  28922  vcdi  28923  vcdir  28924  vcass  28925  nvs  29021  nvz  29027  nvtri  29028  mdbr3  30655  mdbr4  30656  mdsl1i  30679  dmdbr6ati  30781  dmdbr7ati  30782  disjunsn  30929  hasheuni  32049  sigaclcu2  32084  prsiga  32095  measvunilem  32176  cntmeas  32190  omssubadd  32263  signsply0  32526  bnj1498  33037  nummin  33059  lfuhgr2  33076  cvmsdisj  33228  cvmshmeo  33229  cvmliftlem15  33256  cvmlift2lem12  33272  untangtr  33651  elpotr  33753  dfon2lem7  33761  dfon2lem8  33762  tfisg  33782  xpord2ind  33790  xpord3ind  33796  poseq  33798  naddcllem  33827  naddcom  33831  naddid1  33832  madebdayim  34066  opnrebl2  34506  fnemeet2  34552  fnejoin1  34553  fnejoin2  34554  dfgcd3  35491  domalom  35571  ctbssinf  35573  nlpfvineqsn  35576  fvineqsnf1  35577  pibt1  35583  pibt2  35584  ptrecube  35773  poimirlem25  35798  poimirlem26  35799  poimirlem27  35800  poimirlem30  35803  poimirlem31  35804  poimirlem32  35805  heicant  35808  ovoliunnfl  35815  voliunnfl  35817  volsupnfl  35818  frinfm  35889  caushft  35915  sstotbnd3  35930  prdstotbnd  35948  heibor1lem  35963  bfplem2  35977  opidonOLD  36006  exidu1  36010  grpomndo  36029  rngoideu  36057  rngodi  36058  rngodir  36059  rngoass  36060  rngoueqz  36094  idladdcl  36173  idllmulcl  36174  idlrmulcl  36175  mpobi123f  36316  iineq12f  36318  mptbi12f  36320  pmapglbx  37779  ltrnnid  38146  cdlemefrs32fva  38410  fsuppind  40276  dffltz  40468  lerabdioph  40624  ltrabdioph  40627  nerabdioph  40628  dvdsrabdioph  40629  rencldnfi  40640  dford3  40847  pwelg  41137  pwinfi2  41139  ss2iundf  41237  neik0imk0p  41616  gneispace  41714  gneispace0nelrn  41720  ismnushort  41889  ralbidar  42033  rexbidar  42034  uzubico2  43079  climuzlem  43255  xlimxrre  43343  2reuimp0  44574  bgoldbtbndlem2  45227  bgoldbtbndlem4  45229  mpoexxg2  45642  iunord  46351