Theorem ralimdva 3174

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 416	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	a2d 29	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)))
4	3	ralimdv2 3171	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142  ∀wral 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3077

This theorem is referenced by:  ralimdv  3176  ralimdvva  3209  wereu2  5644  frpomin  6327  fveqressseq  7060  f1mpt  7245  isores3  7319  caofrss  7699  caoftrn  7701  sorpssuni  7715  sorpssint  7716  onint  7773  xpord3inddlem  8134  smogt  8338  fisupg  9232  ixpfi2  9293  fissuni  9300  indexfi  9303  fiinfg  9447  wemaplem2  9495  rankonidlem  9786  ac5num  9992  acni2  10002  acndom2  10010  alephle  10044  dfac5  10085  cfsmolem  10227  isf34lem7  10336  isf34lem6  10337  fin1a2s  10371  acncc  10397  ttukeylem6  10471  fpwwe2lem7  10595  gchina  10657  inar1  10733  tskord  10738  grudomon  10775  grur1a  10777  dedekind  11346  fimaxre  12136  fiminre  12139  uzwo  12912  xrsupsslem  13310  xrinfmsslem  13311  fsuppmapnn0fiub0  14006  rexanre  15374  rexuz3  15376  rexico  15381  cau3lem  15382  limsupval2  15507  rlim2lt  15524  rlim3  15525  lo1bdd2  15551  lo1bddrp  15552  o1lo1  15564  climrlim2  15574  2clim  15599  o1co  15613  rlimcn1  15615  rlimcn3  15617  climcn1  15619  climcn2  15620  subcn2  15622  o1of2  15640  rlimo1  15644  o1rlimmul  15646  lo1add  15654  lo1mul  15655  climsqz  15668  climsqz2  15669  rlimsqzlem  15676  lo1le  15679  climbdd  15699  caucvgrlem  15700  caucvgrlem2  15702  caurcvg2  15705  iseralt  15712  cvgcmp  15844  cvgcmpce  15846  gcdcllem1  16533  absproddvds  16651  coprmprod  16695  coprmproddvdslem  16696  pcfac  16935  pockthg  16942  infpnlem1  16946  prmreclem2  16953  prmreclem3  16954  vdwlem11  17027  vdwlem13  17029  vdwnnlem3  17033  isacs2  17685  acsfn1  17693  acsfn2  17695  catpropd  17741  drsdirfi  18337  ipodrsima  18573  isacs5  18580  mrelatglb  18592  mrelatlub  18594  isgrpinv  19035  dfgrp3e  19082  issubg4  19187  gsmsymgreqlem2  19471  finodsubmsubg  19607  gexdvds  19624  gexcl3  19627  sylow2blem3  19662  cyggeninv  19923  gsummptnn0fz  20026  dprdff  20054  issubdrg  20829  acsfn1p  20848  cygznlem3  21621  psdmul  22231  mptcoe1fsupp  22277  cply1coe0bi  22365  gsummoncoe1  22371  evls1fpws  22432  scmatdmat  22575  mdetdiagid  22660  mdetunilem9  22680  cpmatmcllem  22778  m2cpminvid2lem  22814  decpmatmulsumfsupp  22833  pmatcollpw1lem1  22834  pmatcollpw2lem  22837  pmatcollpwfi  22842  pm2mpf1  22859  mptcoe1matfsupp  22862  mp2pm2mplem4  22869  pm2mpmhmlem1  22878  pm2mp  22885  chpdmat  22901  chpscmat  22902  cpmidpmatlem3  22932  cayhamlem4  22948  neiptopnei  23192  cncnp  23340  isnrm2  23418  isreg2  23437  2ndcdisj  23516  islly2  23544  dislly  23557  kgen2ss  23615  ptbasfi  23641  ptclsg  23675  prdstopn  23688  txtube  23700  txlm  23708  isr0  23797  filuni  23945  alexsubALTlem3  24109  ptcmplem3  24114  ptcmplem4  24115  tsmsxplem1  24213  prdsmet  24430  metequiv2  24570  metcnpi3  24606  nmoleub  24791  rescncf  24959  cncfco  24969  evth  25021  lebnumlem3  25025  xlebnum  25027  nmoleub2lem2  25178  nmhmcn  25182  lmmcvg  25323  cmetcaulem  25350  caubl  25370  bcth3  25393  ovollb2lem  25550  ovoliunlem2  25565  ovolicc2lem3  25581  ovolicc2lem4  25582  nulmbl2  25598  volsup  25618  ioombl1lem4  25623  dyadmax  25660  vitalilem2  25671  vitalilem5  25674  mbfi1flimlem  25784  itg2seq  25804  itg2addlem  25820  itgcn  25907  limciun  25956  rolle  26052  dvfsumrlim  26093  itgsubst  26111  aannenlem1  26392  aalioulem3  26398  ulmcaulem  26457  ulmcau  26458  ulmss  26460  ulmbdd  26461  ulmcn  26462  ulmdvlem3  26465  mtest  26467  iblulm  26470  itgulm  26471  rlimcnp  27030  xrlimcnp  27033  rlimcxp  27038  o1cxp  27039  amgm  27055  lgambdd  27101  ftalem2  27138  isppw2  27179  mumullem2  27244  2sqlem6  27487  chtppilimlem2  27538  chtppilim  27539  pntrsumbnd2  27631  pntlem3  27673  nosupbnd1lem5  27776  noinfbnd1lem5  27791  noetasuplem4  27800  noetainflem4  27804  negbdaylem  28149  mulsuniflem  28242  elreno2  28588  isperp2  28888  axeuclidlem  29163  axeuclid  29164  uhgrnbgr0nb  29555  vtxdginducedm1fi  29745  cusgrrusgr  29782  rusgrpropnb  29784  rusgrpropedg  29785  rusgrpropadjvtx  29786  upgrewlkle2  29807  wlkvtxiedg  29825  upgrwlkvtxedg  29845  uspgr2wlkeq  29846  redwlk  29871  wlkdlem2  29882  lfgrwlkprop  29886  2pthnloop  29931  upgr2pthnlp  29932  pthdlem1  29966  pthdlem2lem  29967  wlkiswwlks1  30067  wlkiswwlks2lem4  30072  wwlksm1edg  30081  wwlksnred  30092  clwwlkccatlem  30191  clwlkclwwlklem2a  30200  clwlkclwwlklem2  30202  cusconngr  30393  eucrctshift  30445  2pthfrgr  30486  3cyclfrgr  30490  nmoub3i  30976  ubthlem1  31073  ubthlem3  31075  ocsh  31486  chintcli  31534  chscllem2  31841  nmopub2tALT  32112  nmfnleub2  32129  lnconi  32236  riesz1  32268  rnbra  32310  leopadd  32335  leopmuli  32336  leoptr  32340  dmdbr3  32508  dmdbr4  32509  dmdbr5  32511  mdsl0  32513  mdsymlem6  32611  cdj1i  32636  acunirnmpt  32861  xrge0infss  32962  isdrng4  33482  elrspunidl  33614  dflring2  33689  cmppcmp  34155  zarclsiin  34168  lmxrge0  34249  ftc2re  34892  cvmlift2lem12  35664  opnrebl2  36681  neibastop1  36719  neibastop2lem  36720  neibastop3  36722  finixpnum  38104  lindsenlbs  38114  matunitlindflem1  38115  matunitlindflem2  38116  ptrecube  38119  poimirlem26  38145  poimirlem27  38146  poimirlem29  38148  poimirlem30  38149  poimir  38152  heicant  38154  itg2addnclem  38170  itg2addnclem3  38172  itg2addnc  38173  filbcmb  38239  nninfnub  38250  geomcau  38258  sstotbnd2  38273  isbndx  38281  prdsbnd  38292  heibor1lem  38308  heiborlem1  38310  heibor  38320  rrncmslem  38331  intidl  38528  pclclN  40515  lauteq  40719  ltrnid  40759  mapdh9a  42413  primrootscoprmpow  42716  sticksstones3  42765  aks5lem5a  42808  aks5lem6  42809  fltaccoprm  43222  fltabcoprm  43224  flt4lem5  43232  elrfirn2  43277  isnacs3  43291  rencldnfilem  43397  kelac1  43640  naddgeoa  43971  neik0pk1imk0  44623  cvgdvgrat  44889  neglimc  46221  limsupub  46278  limsuppnflem  46284  limsupre3lem  46306  limsupvaluz2  46312  supcnvlimsup  46314  climuzlem  46317  liminfval2  46342  limsupgtlem  46351  liminflelimsupuz  46359  liminflimsupclim  46381  xlimpnfxnegmnf  46388  liminflimsupxrre  46391  xlimmnfv  46408  xlimpnfv  46412  stoweidlem7  46581  fourierdlem73  46753  sge0isum  47001  meaiuninc3v  47058  preimageiingt  47294  preimaleiinlt  47295  smflimlem3  47347  smflimlem4  47348  cfsetsnfsetfo  47654  2reu8i  47707  iccpartres  48024  uhgrimisgrgric  48553  grlictr  48637  clnbgr3stgrgrlim  48641  clnbgr3stgrgrlic  48642  upwlkwlk  48761  upgrwlkupwlk  48762  copisnmnd  48791  2zrngnmlid2  48879  ply1mulgsumlem1  49008  ply1mulgsumlem3  49010  ply1mulgsumlem4  49011  snlindsntor  49093  eenglngeehlnmlem1  49359  eenglngeehlnmlem2  49360  iinfsubc  49679