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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3067

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

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

This theorem is referenced by:  rexbi  3110  ralrexbid  3112  r19.35OLD  3115  r19.26  3117  r19.29OLD  3121  r19.30  3126  r19.30OLD  3127  2ralimi  3129  3ralimi  3130  4ralimi  3131  5ralimi  3132  6ralimi  3133  r19.21v  3186  rr19.3v  3680  rr19.28v  3681  reu3  3749  uniiunlem  4110  reupick2  4350  ralf0  4537  uniss2  4965  ss2iun  5033  iineq2  5035  dfiun2g  5053  iunss2  5072  disjss2  5136  disjeq2  5137  triin  5300  reusv2lem5  5420  dmmptg  6273  frpoinsg  6375  wfisgOLD  6386  fununi  6653  fnmptf  6716  fnmpt  6720  mpteqb  7048  chfnrn  7082  fvn0ssdmfun  7108  dffo5  7138  ffvresb  7159  fmptcof  7164  mpo2eqb  7582  ralrnmpo  7589  abnexg  7791  tfisg  7891  tfis  7892  fun11uni  7973  fiun  7983  f1iun  7984  zfrep6  7995  mpoexxg  8116  el2mpocsbcl  8126  frxp  8167  xpord2indlem  8188  xpord3inddlem  8195  poseq  8199  smores  8408  naddcllem  8732  naddcom  8738  naddrid  8739  naddunif  8749  naddass  8752  riiner  8848  ixpn0  8988  boxriin  8998  unifi2  9413  wemaplem2  9616  frinsg  9820  rankonidlem  9897  acni3  10116  dfac5  10198  dfac12lem2  10214  kmlem6  10225  kmlem8  10227  kmlem13  10232  cfsmolem  10339  fin23lem40  10420  isf32lem2  10423  fin1a2s  10483  hsmexlem2  10496  hsmex3  10503  axcc4  10508  domtriomlem  10511  dcomex  10516  ac6num  10548  iundom  10611  unirnfdomd  10636  konigthlem  10637  iunctb  10643  gch3  10745  wununi  10775  wunpw  10776  wunpr  10778  eltsk2g  10820  tskpwss  10821  tskpw  10822  grupw  10864  gruurn  10867  intgru  10883  grothpw  10895  grothpwex  10896  grothomex  10898  axgroth3  10900  suplem1pr  11121  supexpr  11123  supsr  11181  fimaxre3  12241  xrsupexmnf  13367  xrinfmexpnf  13368  fsuppmapnn0fiublem  14041  fsuppmapnn0fiub  14042  fsuppmapnn0fiubex  14043  mptnn0fsuppd  14049  rexanre  15395  rexuz3  15397  cau3lem  15403  caubnd2  15406  caubnd  15407  rlim0  15554  rlim0lt  15555  climi2  15557  climi0  15558  climrlim2  15593  rlimres  15604  o1rlimmul  15665  caurcvg  15725  caurcvg2  15726  caucvg  15727  caucvgb  15728  sumeq2  15742  prodeq2  15960  ndvdssub  16457  gcdcllem1  16545  coprmproddvdslem  16709  vdwnnlem1  17042  imasaddfnlem  17588  catidex  17732  catlid  17741  catrid  17742  catcocl  17743  catpropd  17767  subcidcl  17908  funcid  17934  setcepi  18155  tsrss  18659  mgmidmo  18698  gsumval2  18724  isnmnd  18776  issubg2  19181  gagrpid  19334  gaass  19337  cygabl  19933  dprdcntz  20052  dprddisj  20053  abveq0  20841  abvmul  20844  abvtri  20845  psgndiflemB  21641  phllmhm  21673  ipcj  21675  ipeq0  21679  mdetmul  22650  pmatcollpw2lem  22804  eltg2b  22987  iincld  23068  iuncld  23074  isclo2  23117  neips  23142  neipeltop  23158  lmcvg  23291  t1t0  23377  hauscmplem  23435  bwth  23439  1stcelcls  23490  ptuni2  23605  pttopon  23625  ptcld  23642  ptcnplem  23650  txtube  23669  txlm  23677  xkococnlem  23688  fbun  23869  isfil2  23885  ptcmplem4  24084  ustssel  24235  isucn2  24309  ucncn  24315  metrest  24558  tngngp  24696  tngngp3  24698  ncvsi  25204  iscau4  25332  cmetcaulem  25341  caussi  25350  volfiniun  25601  iunmbl  25607  voliun  25608  mbfdm  25680  itg2seq  25797  itg2i1fseqle  25809  itg2i1fseq2  25811  iblcnlem  25844  limcresi  25940  limciun  25949  rolle  26048  ulmss  26458  rlimcnp  27026  madebdayim  27944  addsuniflem  28052  colinearalg  28943  axpasch  28974  axeuclid  28996  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  axcontlem8  29004  fusgrregdegfi  29605  0grrgr  29616  rusgr1vtxlem  29623  wlkvtxeledg  29660  wlkdlem3  29720  wlkdlem4  29721  lfgriswlk  29724  lfgrwlknloop  29725  eulercrct  30274  1to3vfriendship  30313  frgrregorufr0  30356  isgrpo  30529  grpoidinv  30540  grpoideu  30541  grpoidval  30545  grpoidinv2  30547  vcidOLD  30596  vcdi  30597  vcdir  30598  vcass  30599  nvs  30695  nvz  30701  nvtri  30702  mdbr3  32329  mdbr4  32330  mdsl1i  32353  dmdbr6ati  32455  dmdbr7ati  32456  disjunsn  32616  hasheuni  34049  sigaclcu2  34084  prsiga  34095  measvunilem  34176  cntmeas  34190  omssubadd  34265  signsply0  34528  bnj1498  35037  nummin  35067  lfuhgr2  35086  cvmsdisj  35238  cvmshmeo  35239  cvmliftlem15  35266  cvmlift2lem12  35282  untangtr  35676  elpotr  35745  dfon2lem7  35753  dfon2lem8  35754  opnrebl2  36287  fnemeet2  36333  fnejoin1  36334  fnejoin2  36335  weiunso  36432  weiunse  36434  weiunwe  36435  dfgcd3  37290  domalom  37370  ctbssinf  37372  nlpfvineqsn  37375  fvineqsnf1  37376  pibt1  37382  pibt2  37383  ptrecube  37580  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  heicant  37615  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  frinfm  37695  caushft  37721  sstotbnd3  37736  prdstotbnd  37754  heibor1lem  37769  bfplem2  37783  opidonOLD  37812  exidu1  37816  grpomndo  37835  rngoideu  37863  rngodi  37864  rngodir  37865  rngoass  37866  rngoueqz  37900  idladdcl  37979  idllmulcl  37980  idlrmulcl  37981  mpobi123f  38122  iineq12f  38124  mptbi12f  38126  pmapglbx  39726  ltrnnid  40093  cdlemefrs32fva  40357  unitscyglem3  42154  fsuppind  42545  dffltz  42589  lerabdioph  42761  ltrabdioph  42764  nerabdioph  42765  dvdsrabdioph  42766  rencldnfi  42777  dford3  42985  pwelg  43522  pwinfi2  43524  ss2iundf  43621  neik0imk0p  43998  gneispace  44096  gneispace0nelrn  44102  ismnushort  44270  ralbidar  44414  rexbidar  44415  uzubico2  45488  climuzlem  45664  xlimxrre  45752  natlocalincr  46795  2reuimp0  47029  bgoldbtbndlem2  47680  bgoldbtbndlem4  47682  mpoexxg2  48062  iunord  48768