Theorem ralimdva 3177

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3143

This theorem is referenced by:  ralimdv  3178  ralimdvva  3179  wereu2  5547  fveqressseq  6842  f1mpt  7013  isores3  7082  caofrss  7436  caoftrn  7438  sorpssuni  7452  sorpssint  7453  onint  7504  smogt  7998  fisupg  8760  ixpfi2  8816  fissuni  8823  indexfi  8826  fiinfg  8957  wemaplem2  9005  rankonidlem  9251  ac5num  9456  acni2  9466  acndom2  9474  alephle  9508  dfac5  9548  cfsmolem  9686  isf34lem7  9795  isf34lem6  9796  fin1a2s  9830  acncc  9856  ttukeylem6  9930  fpwwe2lem8  10053  gchina  10115  inar1  10191  tskord  10196  grudomon  10233  grur1a  10235  dedekind  10797  fimaxre  11578  fimaxreOLD  11579  fiminre  11582  uzwo  12305  xrsupsslem  12694  xrinfmsslem  12695  fsuppmapnn0fiub0  13355  rexanre  14700  rexuz3  14702  rexico  14707  cau3lem  14708  limsupval2  14831  rlim2lt  14848  rlim3  14849  lo1bdd2  14875  lo1bddrp  14876  o1lo1  14888  climrlim2  14898  2clim  14923  o1co  14937  rlimcn1  14939  rlimcn2  14941  climcn1  14942  climcn2  14943  subcn2  14945  o1of2  14963  rlimo1  14967  o1rlimmul  14969  lo1add  14977  lo1mul  14978  climsqz  14991  climsqz2  14992  rlimsqzlem  14999  lo1le  15002  climbdd  15022  caucvgrlem  15023  caucvgrlem2  15025  caurcvg2  15028  iseralt  15035  cvgcmp  15165  cvgcmpce  15167  gcdcllem1  15842  absproddvds  15955  coprmprod  15999  coprmproddvdslem  16000  pcfac  16229  pockthg  16236  infpnlem1  16240  prmreclem2  16247  prmreclem3  16248  vdwlem11  16321  vdwlem13  16323  vdwnnlem3  16327  isacs2  16918  acsfn1  16926  acsfn2  16928  catpropd  16973  drsdirfi  17542  ipodrsima  17769  isacs5  17776  mrelatglb  17788  mrelatlub  17790  isgrpinv  18150  dfgrp3e  18193  issubg4  18292  gsmsymgreqlem2  18553  gexdvds  18703  gexcl3  18706  sylow2blem3  18741  cyggeninv  18996  gsummptnn0fz  19100  dprdff  19128  issubdrg  19554  acsfn1p  19572  mptcoe1fsupp  20377  cply1coe0bi  20462  gsummoncoe1  20466  cygznlem3  20710  scmatdmat  21118  mdetdiagid  21203  mdetunilem9  21223  cpmatmcllem  21320  m2cpminvid2lem  21356  decpmatmulsumfsupp  21375  pmatcollpw1lem1  21376  pmatcollpw2lem  21379  pmatcollpwfi  21384  pm2mpf1  21401  mptcoe1matfsupp  21404  mp2pm2mplem4  21411  pm2mpmhmlem1  21420  pm2mp  21427  chpdmat  21443  chpscmat  21444  cpmidpmatlem3  21474  cayhamlem4  21490  neiptopnei  21734  cncnp  21882  isnrm2  21960  isreg2  21979  2ndcdisj  22058  islly2  22086  dislly  22099  kgen2ss  22157  ptbasfi  22183  ptclsg  22217  prdstopn  22230  txtube  22242  txlm  22250  isr0  22339  filuni  22487  alexsubALTlem3  22651  ptcmplem3  22656  ptcmplem4  22657  tsmsxplem1  22755  prdsmet  22974  metequiv2  23114  metcnpi3  23150  nmoleub  23334  rescncf  23499  cncfco  23509  evth  23557  lebnumlem3  23561  xlebnum  23563  nmoleub2lem2  23714  nmhmcn  23718  lmmcvg  23858  cmetcaulem  23885  caubl  23905  bcth3  23928  ovollb2lem  24083  ovoliunlem2  24098  ovolicc2lem3  24114  ovolicc2lem4  24115  nulmbl2  24131  volsup  24151  ioombl1lem4  24156  dyadmax  24193  vitalilem2  24204  vitalilem5  24207  mbfi1flimlem  24317  itg2seq  24337  itg2addlem  24353  itgcn  24437  limciun  24486  rolle  24581  dvfsumrlim  24622  itgsubst  24640  aannenlem1  24911  aalioulem3  24917  ulmcaulem  24976  ulmcau  24977  ulmss  24979  ulmbdd  24980  ulmcn  24981  ulmdvlem3  24984  mtest  24986  iblulm  24989  itgulm  24990  rlimcnp  25537  xrlimcnp  25540  rlimcxp  25545  o1cxp  25546  amgm  25562  lgambdd  25608  ftalem2  25645  isppw2  25686  mumullem2  25751  2sqlem6  25993  chtppilimlem2  26044  chtppilim  26045  pntrsumbnd2  26137  pntlem3  26179  isperp2  26495  axeuclidlem  26742  axeuclid  26743  uhgrnbgr0nb  27130  vtxdginducedm1fi  27320  cusgrrusgr  27357  rusgrpropnb  27359  rusgrpropedg  27360  rusgrpropadjvtx  27361  upgrewlkle2  27382  wlkvtxiedg  27400  upgrwlkvtxedg  27420  uspgr2wlkeq  27421  redwlk  27448  wlkdlem2  27459  lfgrwlkprop  27463  2pthnloop  27506  upgr2pthnlp  27507  pthdlem1  27541  pthdlem2lem  27542  wlkiswwlks1  27639  wlkiswwlks2lem4  27644  wwlksm1edg  27653  wwlksnred  27664  clwwlkccatlem  27761  clwlkclwwlklem2a  27770  clwlkclwwlklem2  27772  cusconngr  27964  eucrctshift  28016  2pthfrgr  28057  3cyclfrgr  28061  nmoub3i  28544  ubthlem1  28641  ubthlem3  28643  ocsh  29054  chintcli  29102  chscllem2  29409  nmopub2tALT  29680  nmfnleub2  29697  lnconi  29804  riesz1  29836  rnbra  29878  leopadd  29903  leopmuli  29904  leoptr  29908  dmdbr3  30076  dmdbr4  30077  dmdbr5  30079  mdsl0  30081  mdsymlem6  30179  cdj1i  30204  acunirnmpt  30398  xrge0infss  30478  cmppcmp  31117  lmxrge0  31190  ftc2re  31864  cvmlift2lem12  32556  frpomin  33073  nosupbnd1lem5  33207  noetalem3  33214  opnrebl2  33664  neibastop1  33702  neibastop2lem  33703  neibastop3  33705  finixpnum  34871  lindsenlbs  34881  matunitlindflem1  34882  matunitlindflem2  34883  ptrecube  34886  poimirlem26  34912  poimirlem27  34913  poimirlem29  34915  poimirlem30  34916  poimir  34919  heicant  34921  itg2addnclem  34937  itg2addnclem3  34939  itg2addnc  34940  filbcmb  35009  nninfnub  35020  geomcau  35028  sstotbnd2  35046  isbndx  35054  prdsbnd  35065  heibor1lem  35081  heiborlem1  35083  heibor  35093  rrncmslem  35104  intidl  35301  pclclN  37021  lauteq  37225  ltrnid  37265  mapdh9a  38919  elrfirn2  39286  isnacs3  39300  rencldnfilem  39410  kelac1  39656  neik0pk1imk0  40390  cvgdvgrat  40638  neglimc  41920  limsupub  41977  limsuppnflem  41983  limsupre3lem  42005  limsupvaluz2  42011  supcnvlimsup  42013  climuzlem  42016  liminfval2  42041  limsupgtlem  42050  liminflelimsupuz  42058  liminflimsupclim  42080  xlimpnfxnegmnf  42087  liminflimsupxrre  42090  xlimmnfv  42107  xlimpnfv  42111  stoweidlem7  42285  fourierdlem73  42457  sge0isum  42702  meaiuninc3v  42759  preimageiingt  42991  preimaleiinlt  42992  smflimlem3  43042  smflimlem4  43043  2reu8i  43305  iccpartres  43571  upwlkwlk  44007  upgrwlkupwlk  44008  copisnmnd  44069  2zrngnmlid2  44215  ply1mulgsumlem1  44433  ply1mulgsumlem3  44435  ply1mulgsumlem4  44436  snlindsntor  44519  eenglngeehlnmlem1  44717  eenglngeehlnmlem2  44718