Theorem ralimi 3070

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∀wral 3048

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

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

This theorem is referenced by:  rexbi  3089  ralrexbid  3090  r19.26  3093  r19.30  3100  2ralimi  3103  3ralimi  3104  4ralimi  3105  5ralimi  3106  6ralimi  3107  r19.21v  3158  rr19.3v  3618  rr19.28v  3619  reu3  3682  uniiunlem  4036  reupick2  4280  uniss2  4894  ss2iun  4962  iineq2  4964  dfiun2g  4982  iunss2  5002  disjss2  5065  disjeq2  5066  triin  5218  reusv2lem5  5344  dmmptg  6197  frpoinsg  6298  fununi  6564  fnmptf  6625  fnmpt  6629  mpteqb  6957  chfnrn  6991  fvn0ssdmfun  7016  dffo5  7046  ffvresb  7067  fmptcof  7072  mpo2eqb  7487  ralrnmpo  7494  abnexg  7698  tfisg  7793  tfis  7794  fun11uni  7872  fiun  7884  f1iun  7885  zfrep6  7896  mpoexxg  8016  el2mpocsbcl  8024  frxp  8065  xpord2indlem  8086  xpord3inddlem  8093  poseq  8097  smores  8281  naddcllem  8600  naddcom  8606  naddrid  8607  naddunif  8617  naddass  8620  riiner  8723  ixpn0  8864  boxriin  8874  unifi2  9240  wemaplem2  9444  frinsg  9655  rankonidlem  9732  acni3  9949  dfac5  10031  dfac12lem2  10047  kmlem6  10058  kmlem8  10060  kmlem13  10065  cfsmolem  10172  fin23lem40  10253  isf32lem2  10256  fin1a2s  10316  hsmexlem2  10329  hsmex3  10336  axcc4  10341  domtriomlem  10344  dcomex  10349  ac6num  10381  iundom  10444  unirnfdomd  10469  konigthlem  10470  iunctb  10476  gch3  10578  wununi  10608  wunpw  10609  wunpr  10611  eltsk2g  10653  tskpwss  10654  tskpw  10655  grupw  10697  gruurn  10700  intgru  10716  grothpw  10728  grothpwex  10729  grothomex  10731  axgroth3  10733  suplem1pr  10954  supexpr  10956  supsr  11014  fimaxre3  12079  xrsupexmnf  13211  xrinfmexpnf  13212  fsuppmapnn0fiublem  13904  fsuppmapnn0fiub  13905  fsuppmapnn0fiubex  13906  mptnn0fsuppd  13912  rexanre  15261  rexuz3  15263  cau3lem  15269  caubnd2  15272  caubnd  15273  rlim0  15422  rlim0lt  15423  climi2  15425  climi0  15426  climrlim2  15461  rlimres  15472  o1rlimmul  15533  caurcvg  15591  caurcvg2  15592  caucvg  15593  caucvgb  15594  sumeq2  15608  prodeq2  15826  ndvdssub  16327  gcdcllem1  16417  coprmproddvdslem  16580  vdwnnlem1  16914  imasaddfnlem  17440  catidex  17588  catlid  17597  catrid  17598  catcocl  17599  catpropd  17623  subcidcl  17759  funcid  17785  setcepi  18003  tsrss  18503  mgmidmo  18576  gsumval2  18602  isnmnd  18654  issubg2  19062  gagrpid  19214  gaass  19217  cygabl  19811  dprdcntz  19930  dprddisj  19931  abveq0  20742  abvmul  20745  abvtri  20746  psgndiflemB  21546  phllmhm  21578  ipcj  21580  ipeq0  21584  mdetmul  22558  pmatcollpw2lem  22712  eltg2b  22894  iincld  22974  iuncld  22980  isclo2  23023  neips  23048  neipeltop  23064  lmcvg  23197  t1t0  23283  hauscmplem  23341  bwth  23345  1stcelcls  23396  ptuni2  23511  pttopon  23531  ptcld  23548  ptcnplem  23556  txtube  23575  txlm  23583  xkococnlem  23594  fbun  23775  isfil2  23791  ptcmplem4  23990  ustssel  24141  isucn2  24213  ucncn  24219  metrest  24459  tngngp  24589  tngngp3  24591  ncvsi  25098  iscau4  25226  cmetcaulem  25235  caussi  25244  volfiniun  25495  iunmbl  25501  voliun  25502  mbfdm  25574  itg2seq  25690  itg2i1fseqle  25702  itg2i1fseq2  25704  iblcnlem  25737  limcresi  25833  limciun  25842  rolle  25941  ulmss  26353  rlimcnp  26922  madebdayim  27853  addsuniflem  27964  colinearalg  28909  axpasch  28940  axeuclid  28962  axcontlem2  28964  axcontlem4  28966  axcontlem7  28969  axcontlem8  28970  fusgrregdegfi  29569  0grrgr  29580  rusgr1vtxlem  29587  wlkvtxeledg  29623  wlkdlem3  29682  wlkdlem4  29683  lfgriswlk  29686  lfgrwlknloop  29687  eulercrct  30243  1to3vfriendship  30282  frgrregorufr0  30325  isgrpo  30498  grpoidinv  30509  grpoideu  30510  grpoidval  30514  grpoidinv2  30516  vcidOLD  30565  vcdi  30566  vcdir  30567  vcass  30568  nvs  30664  nvz  30670  nvtri  30671  mdbr3  32298  mdbr4  32299  mdsl1i  32322  dmdbr6ati  32424  dmdbr7ati  32425  disjunsn  32595  hasheuni  34170  sigaclcu2  34205  prsiga  34216  measvunilem  34297  cntmeas  34311  omssubadd  34385  signsply0  34636  bnj1498  35145  nummin  35176  tz9.1regs  35202  onvf1odlem4  35222  lfuhgr2  35235  cvmsdisj  35386  cvmshmeo  35387  cvmliftlem15  35414  cvmlift2lem12  35430  untangtr  35830  elpotr  35895  dfon2lem7  35903  dfon2lem8  35904  opnrebl2  36437  fnemeet2  36483  fnejoin1  36484  fnejoin2  36485  weiunso  36582  weiunse  36584  weiunwe  36585  dfgcd3  37441  domalom  37521  ctbssinf  37523  nlpfvineqsn  37526  fvineqsnf1  37527  pibt1  37533  pibt2  37534  ptrecube  37733  poimirlem25  37758  poimirlem26  37759  poimirlem27  37760  poimirlem30  37763  poimirlem31  37764  poimirlem32  37765  heicant  37768  ovoliunnfl  37775  voliunnfl  37777  volsupnfl  37778  frinfm  37848  caushft  37874  sstotbnd3  37889  prdstotbnd  37907  heibor1lem  37922  bfplem2  37936  opidonOLD  37965  exidu1  37969  grpomndo  37988  rngoideu  38016  rngodi  38017  rngodir  38018  rngoass  38019  rngoueqz  38053  idladdcl  38132  idllmulcl  38133  idlrmulcl  38134  mpobi123f  38275  iineq12f  38277  mptbi12f  38279  dmqsblocks  39024  pmapglbx  39941  ltrnnid  40308  cdlemefrs32fva  40572  unitscyglem3  42363  fsuppind  42748  dffltz  42792  lerabdioph  42962  ltrabdioph  42965  nerabdioph  42966  dvdsrabdioph  42967  rencldnfi  42978  dford3  43185  pwelg  43717  pwinfi2  43719  ss2iundf  43816  neik0imk0p  44193  gneispace  44291  gneispace0nelrn  44297  ismnushort  44458  ralbidar  44601  rexbidar  44602  ssclaxsep  45139  uniclaxun  45143  uzubico2  45730  climuzlem  45903  xlimxrre  45991  natlocalincr  47036  2reuimp0  47276  bgoldbtbndlem2  47968  bgoldbtbndlem4  47970  mpoexxg2  48500  iuneqconst2  48984  iineqconst2  48985  iunord  49837