Theorem ralimdva 3153

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-an 398  df-ral 3056

This theorem is referenced by:  ralimdv  3155  ralimdvva  3188  wereu2  5617  frpomin  6294  fveqressseq  7023  f1mpt  7208  isores3  7282  caofrss  7662  caoftrn  7664  sorpssuni  7678  sorpssint  7679  onint  7736  xpord3inddlem  8096  smogt  8300  fisupg  9192  ixpfi2  9254  fissuni  9261  indexfi  9264  fiinfg  9408  wemaplem2  9456  rankonidlem  9747  ac5num  9953  acni2  9963  acndom2  9971  alephle  10005  dfac5  10046  cfsmolem  10188  isf34lem7  10297  isf34lem6  10298  fin1a2s  10332  acncc  10358  ttukeylem6  10432  fpwwe2lem7  10556  gchina  10618  inar1  10694  tskord  10699  grudomon  10736  grur1a  10738  dedekind  11305  fimaxre  12095  fiminre  12098  uzwo  12856  xrsupsslem  13254  xrinfmsslem  13255  fsuppmapnn0fiub0  13950  rexanre  15304  rexuz3  15306  rexico  15311  cau3lem  15312  limsupval2  15437  rlim2lt  15454  rlim3  15455  lo1bdd2  15481  lo1bddrp  15482  o1lo1  15494  climrlim2  15504  2clim  15529  o1co  15543  rlimcn1  15545  rlimcn3  15547  climcn1  15549  climcn2  15550  subcn2  15552  o1of2  15570  rlimo1  15574  o1rlimmul  15576  lo1add  15584  lo1mul  15585  climsqz  15598  climsqz2  15599  rlimsqzlem  15606  lo1le  15609  climbdd  15629  caucvgrlem  15630  caucvgrlem2  15632  caurcvg2  15635  iseralt  15642  cvgcmp  15774  cvgcmpce  15776  gcdcllem1  16463  absproddvds  16581  coprmprod  16625  coprmproddvdslem  16626  pcfac  16865  pockthg  16872  infpnlem1  16876  prmreclem2  16883  prmreclem3  16884  vdwlem11  16957  vdwlem13  16959  vdwnnlem3  16963  isacs2  17614  acsfn1  17622  acsfn2  17624  catpropd  17670  drsdirfi  18266  ipodrsima  18502  isacs5  18509  mrelatglb  18521  mrelatlub  18523  isgrpinv  18964  dfgrp3e  19011  issubg4  19116  gsmsymgreqlem2  19400  finodsubmsubg  19536  gexdvds  19553  gexcl3  19556  sylow2blem3  19591  cyggeninv  19852  gsummptnn0fz  19955  dprdff  19983  issubdrg  20755  acsfn1p  20774  cygznlem3  21547  psdmul  22157  mptcoe1fsupp  22203  cply1coe0bi  22291  gsummoncoe1  22297  evls1fpws  22358  scmatdmat  22501  mdetdiagid  22586  mdetunilem9  22606  cpmatmcllem  22704  m2cpminvid2lem  22740  decpmatmulsumfsupp  22759  pmatcollpw1lem1  22760  pmatcollpw2lem  22763  pmatcollpwfi  22768  pm2mpf1  22785  mptcoe1matfsupp  22788  mp2pm2mplem4  22795  pm2mpmhmlem1  22804  pm2mp  22811  chpdmat  22827  chpscmat  22828  cpmidpmatlem3  22858  cayhamlem4  22874  neiptopnei  23118  cncnp  23266  isnrm2  23344  isreg2  23363  2ndcdisj  23442  islly2  23470  dislly  23483  kgen2ss  23541  ptbasfi  23567  ptclsg  23601  prdstopn  23614  txtube  23626  txlm  23634  isr0  23723  filuni  23871  alexsubALTlem3  24035  ptcmplem3  24040  ptcmplem4  24041  tsmsxplem1  24139  prdsmet  24356  metequiv2  24496  metcnpi3  24532  nmoleub  24717  rescncf  24885  cncfco  24895  evth  24947  lebnumlem3  24951  xlebnum  24953  nmoleub2lem2  25104  nmhmcn  25108  lmmcvg  25249  cmetcaulem  25276  caubl  25296  bcth3  25319  ovollb2lem  25476  ovoliunlem2  25491  ovolicc2lem3  25507  ovolicc2lem4  25508  nulmbl2  25524  volsup  25544  ioombl1lem4  25549  dyadmax  25586  vitalilem2  25597  vitalilem5  25600  mbfi1flimlem  25710  itg2seq  25730  itg2addlem  25746  itgcn  25833  limciun  25882  rolle  25978  dvfsumrlim  26019  itgsubst  26037  aannenlem1  26315  aalioulem3  26321  ulmcaulem  26380  ulmcau  26381  ulmss  26383  ulmbdd  26384  ulmcn  26385  ulmdvlem3  26388  mtest  26390  iblulm  26393  itgulm  26394  rlimcnp  26950  xrlimcnp  26953  rlimcxp  26958  o1cxp  26959  amgm  26975  lgambdd  27021  ftalem2  27058  isppw2  27099  mumullem2  27164  2sqlem6  27407  chtppilimlem2  27458  chtppilim  27459  pntrsumbnd2  27551  pntlem3  27593  nosupbnd1lem5  27696  noinfbnd1lem5  27711  noetasuplem4  27720  noetainflem4  27724  negbdaylem  28068  mulsuniflem  28161  elreno2  28507  isperp2  28803  axeuclidlem  29051  axeuclid  29052  uhgrnbgr0nb  29443  vtxdginducedm1fi  29633  cusgrrusgr  29670  rusgrpropnb  29672  rusgrpropedg  29673  rusgrpropadjvtx  29674  upgrewlkle2  29695  wlkvtxiedg  29713  upgrwlkvtxedg  29733  uspgr2wlkeq  29734  redwlk  29759  wlkdlem2  29770  lfgrwlkprop  29774  2pthnloop  29819  upgr2pthnlp  29820  pthdlem1  29854  pthdlem2lem  29855  wlkiswwlks1  29955  wlkiswwlks2lem4  29960  wwlksm1edg  29969  wwlksnred  29980  clwwlkccatlem  30079  clwlkclwwlklem2a  30088  clwlkclwwlklem2  30090  cusconngr  30281  eucrctshift  30333  2pthfrgr  30374  3cyclfrgr  30378  nmoub3i  30864  ubthlem1  30961  ubthlem3  30963  ocsh  31374  chintcli  31422  chscllem2  31729  nmopub2tALT  32000  nmfnleub2  32017  lnconi  32124  riesz1  32156  rnbra  32198  leopadd  32223  leopmuli  32224  leoptr  32228  dmdbr3  32396  dmdbr4  32397  dmdbr5  32399  mdsl0  32401  mdsymlem6  32499  cdj1i  32524  acunirnmpt  32753  xrge0infss  32854  isdrng4  33381  elrspunidl  33513  dflring2  33586  cmppcmp  34052  zarclsiin  34065  lmxrge0  34146  ftc2re  34792  cvmlift2lem12  35555  opnrebl2  36562  neibastop1  36600  neibastop2lem  36601  neibastop3  36603  finixpnum  37985  lindsenlbs  37995  matunitlindflem1  37996  matunitlindflem2  37997  ptrecube  38000  poimirlem26  38026  poimirlem27  38027  poimirlem29  38029  poimirlem30  38030  poimir  38033  heicant  38035  itg2addnclem  38051  itg2addnclem3  38053  itg2addnc  38054  filbcmb  38120  nninfnub  38131  geomcau  38139  sstotbnd2  38154  isbndx  38162  prdsbnd  38173  heibor1lem  38189  heiborlem1  38191  heibor  38201  rrncmslem  38212  intidl  38409  pclclN  40396  lauteq  40600  ltrnid  40640  mapdh9a  42294  primrootscoprmpow  42597  sticksstones3  42646  aks5lem5a  42689  aks5lem6  42690  fltaccoprm  43103  fltabcoprm  43105  flt4lem5  43113  elrfirn2  43158  isnacs3  43172  rencldnfilem  43278  kelac1  43521  naddgeoa  43852  neik0pk1imk0  44504  cvgdvgrat  44770  neglimc  46102  limsupub  46159  limsuppnflem  46165  limsupre3lem  46187  limsupvaluz2  46193  supcnvlimsup  46195  climuzlem  46198  liminfval2  46223  limsupgtlem  46232  liminflelimsupuz  46240  liminflimsupclim  46262  xlimpnfxnegmnf  46269  liminflimsupxrre  46272  xlimmnfv  46289  xlimpnfv  46293  stoweidlem7  46462  fourierdlem73  46634  sge0isum  46882  meaiuninc3v  46939  preimageiingt  47175  preimaleiinlt  47176  smflimlem3  47228  smflimlem4  47229  cfsetsnfsetfo  47535  2reu8i  47588  iccpartres  47905  uhgrimisgrgric  48434  grlictr  48518  clnbgr3stgrgrlim  48522  clnbgr3stgrgrlic  48523  upwlkwlk  48642  upgrwlkupwlk  48643  copisnmnd  48672  2zrngnmlid2  48760  ply1mulgsumlem1  48889  ply1mulgsumlem3  48891  ply1mulgsumlem4  48892  snlindsntor  48974  eenglngeehlnmlem1  49240  eenglngeehlnmlem2  49241  iinfsubc  49560