Theorem ralimdva 3150

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

Hypothesis

Ref	Expression
ralimdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
ralimdva	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdva

Step	Hyp	Ref	Expression
1		ralimdva.1	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 412	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	a2d 29	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)))
4	3	ralimdv2 3147	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3053

This theorem is referenced by:  ralimdv  3152  ralimdvva  3185  wereu2  5629  frpomin  6306  fveqressseq  7033  f1mpt  7217  isores3  7291  caofrss  7671  caoftrn  7673  sorpssuni  7687  sorpssint  7688  onint  7745  xpord3inddlem  8106  smogt  8309  fisupg  9200  ixpfi2  9262  fissuni  9269  indexfi  9272  fiinfg  9416  wemaplem2  9464  rankonidlem  9752  ac5num  9958  acni2  9968  acndom2  9976  alephle  10010  dfac5  10051  cfsmolem  10192  isf34lem7  10301  isf34lem6  10302  fin1a2s  10336  acncc  10362  ttukeylem6  10436  fpwwe2lem7  10560  gchina  10622  inar1  10698  tskord  10703  grudomon  10740  grur1a  10742  dedekind  11308  fimaxre  12098  fiminre  12101  uzwo  12836  xrsupsslem  13234  xrinfmsslem  13235  fsuppmapnn0fiub0  13928  rexanre  15282  rexuz3  15284  rexico  15289  cau3lem  15290  limsupval2  15415  rlim2lt  15432  rlim3  15433  lo1bdd2  15459  lo1bddrp  15460  o1lo1  15472  climrlim2  15482  2clim  15507  o1co  15521  rlimcn1  15523  rlimcn3  15525  climcn1  15527  climcn2  15528  subcn2  15530  o1of2  15548  rlimo1  15552  o1rlimmul  15554  lo1add  15562  lo1mul  15563  climsqz  15576  climsqz2  15577  rlimsqzlem  15584  lo1le  15587  climbdd  15607  caucvgrlem  15608  caucvgrlem2  15610  caurcvg2  15613  iseralt  15620  cvgcmp  15751  cvgcmpce  15753  gcdcllem1  16438  absproddvds  16556  coprmprod  16600  coprmproddvdslem  16601  pcfac  16839  pockthg  16846  infpnlem1  16850  prmreclem2  16857  prmreclem3  16858  vdwlem11  16931  vdwlem13  16933  vdwnnlem3  16937  isacs2  17588  acsfn1  17596  acsfn2  17598  catpropd  17644  drsdirfi  18240  ipodrsima  18476  isacs5  18483  mrelatglb  18495  mrelatlub  18497  isgrpinv  18938  dfgrp3e  18985  issubg4  19090  gsmsymgreqlem2  19375  finodsubmsubg  19511  gexdvds  19528  gexcl3  19531  sylow2blem3  19566  cyggeninv  19827  gsummptnn0fz  19930  dprdff  19958  issubdrg  20728  acsfn1p  20747  cygznlem3  21539  psdmul  22124  mptcoe1fsupp  22171  cply1coe0bi  22261  gsummoncoe1  22267  evls1fpws  22328  scmatdmat  22474  mdetdiagid  22559  mdetunilem9  22579  cpmatmcllem  22677  m2cpminvid2lem  22713  decpmatmulsumfsupp  22732  pmatcollpw1lem1  22733  pmatcollpw2lem  22736  pmatcollpwfi  22741  pm2mpf1  22758  mptcoe1matfsupp  22761  mp2pm2mplem4  22768  pm2mpmhmlem1  22777  pm2mp  22784  chpdmat  22800  chpscmat  22801  cpmidpmatlem3  22831  cayhamlem4  22847  neiptopnei  23091  cncnp  23239  isnrm2  23317  isreg2  23336  2ndcdisj  23415  islly2  23443  dislly  23456  kgen2ss  23514  ptbasfi  23540  ptclsg  23574  prdstopn  23587  txtube  23599  txlm  23607  isr0  23696  filuni  23844  alexsubALTlem3  24008  ptcmplem3  24013  ptcmplem4  24014  tsmsxplem1  24112  prdsmet  24329  metequiv2  24469  metcnpi3  24505  nmoleub  24690  rescncf  24861  cncfco  24871  evth  24929  lebnumlem3  24933  xlebnum  24935  nmoleub2lem2  25087  nmhmcn  25091  lmmcvg  25232  cmetcaulem  25259  caubl  25279  bcth3  25302  ovollb2lem  25460  ovoliunlem2  25475  ovolicc2lem3  25491  ovolicc2lem4  25492  nulmbl2  25508  volsup  25528  ioombl1lem4  25533  dyadmax  25570  vitalilem2  25581  vitalilem5  25584  mbfi1flimlem  25694  itg2seq  25714  itg2addlem  25730  itgcn  25817  limciun  25866  rolle  25965  dvfsumrlim  26009  itgsubst  26027  aannenlem1  26307  aalioulem3  26313  ulmcaulem  26374  ulmcau  26375  ulmss  26377  ulmbdd  26378  ulmcn  26379  ulmdvlem3  26382  mtest  26384  iblulm  26387  itgulm  26388  rlimcnp  26946  xrlimcnp  26949  rlimcxp  26955  o1cxp  26956  amgm  26972  lgambdd  27018  ftalem2  27055  isppw2  27096  mumullem2  27161  2sqlem6  27405  chtppilimlem2  27456  chtppilim  27457  pntrsumbnd2  27549  pntlem3  27591  nosupbnd1lem5  27695  noinfbnd1lem5  27710  noetasuplem4  27719  noetainflem4  27723  negbdaylem  28067  mulsuniflem  28160  elreno2  28506  isperp2  28803  axeuclidlem  29051  axeuclid  29052  uhgrnbgr0nb  29443  vtxdginducedm1fi  29634  cusgrrusgr  29671  rusgrpropnb  29673  rusgrpropedg  29674  rusgrpropadjvtx  29675  upgrewlkle2  29696  wlkvtxiedg  29714  upgrwlkvtxedg  29734  uspgr2wlkeq  29735  redwlk  29760  wlkdlem2  29771  lfgrwlkprop  29775  2pthnloop  29820  upgr2pthnlp  29821  pthdlem1  29855  pthdlem2lem  29856  wlkiswwlks1  29956  wlkiswwlks2lem4  29961  wwlksm1edg  29970  wwlksnred  29981  clwwlkccatlem  30080  clwlkclwwlklem2a  30089  clwlkclwwlklem2  30091  cusconngr  30282  eucrctshift  30334  2pthfrgr  30375  3cyclfrgr  30379  nmoub3i  30865  ubthlem1  30962  ubthlem3  30964  ocsh  31375  chintcli  31423  chscllem2  31730  nmopub2tALT  32001  nmfnleub2  32018  lnconi  32125  riesz1  32157  rnbra  32199  leopadd  32224  leopmuli  32225  leoptr  32229  dmdbr3  32397  dmdbr4  32398  dmdbr5  32400  mdsl0  32402  mdsymlem6  32500  cdj1i  32525  acunirnmpt  32753  xrge0infss  32855  isdrng4  33393  elrspunidl  33525  cmppcmp  34040  zarclsiin  34053  lmxrge0  34134  ftc2re  34780  cvmlift2lem12  35534  opnrebl2  36541  neibastop1  36579  neibastop2lem  36580  neibastop3  36582  finixpnum  37860  lindsenlbs  37870  matunitlindflem1  37871  matunitlindflem2  37872  ptrecube  37875  poimirlem26  37901  poimirlem27  37902  poimirlem29  37904  poimirlem30  37905  poimir  37908  heicant  37910  itg2addnclem  37926  itg2addnclem3  37928  itg2addnc  37929  filbcmb  37995  nninfnub  38006  geomcau  38014  sstotbnd2  38029  isbndx  38037  prdsbnd  38048  heibor1lem  38064  heiborlem1  38066  heibor  38076  rrncmslem  38087  intidl  38284  pclclN  40271  lauteq  40475  ltrnid  40515  mapdh9a  42169  primrootscoprmpow  42473  sticksstones3  42522  aks5lem5a  42565  aks5lem6  42566  fltaccoprm  43002  fltabcoprm  43004  flt4lem5  43012  elrfirn2  43057  isnacs3  43071  rencldnfilem  43181  kelac1  43424  naddgeoa  43755  neik0pk1imk0  44407  cvgdvgrat  44673  neglimc  46009  limsupub  46066  limsuppnflem  46072  limsupre3lem  46094  limsupvaluz2  46100  supcnvlimsup  46102  climuzlem  46105  liminfval2  46130  limsupgtlem  46139  liminflelimsupuz  46147  liminflimsupclim  46169  xlimpnfxnegmnf  46176  liminflimsupxrre  46179  xlimmnfv  46196  xlimpnfv  46200  stoweidlem7  46369  fourierdlem73  46541  sge0isum  46789  meaiuninc3v  46846  preimageiingt  47082  preimaleiinlt  47083  smflimlem3  47135  smflimlem4  47136  cfsetsnfsetfo  47424  2reu8i  47477  iccpartres  47782  uhgrimisgrgric  48295  grlictr  48379  clnbgr3stgrgrlim  48383  clnbgr3stgrgrlic  48384  upwlkwlk  48503  upgrwlkupwlk  48504  copisnmnd  48533  2zrngnmlid2  48621  ply1mulgsumlem1  48750  ply1mulgsumlem3  48752  ply1mulgsumlem4  48753  snlindsntor  48835  eenglngeehlnmlem1  49101  eenglngeehlnmlem2  49102  iinfsubc  49421