Theorem ralimdva 3148

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3051

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

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

This theorem is referenced by:  ralimdv  3150  ralimdvva  3183  wereu2  5621  frpomin  6298  fveqressseq  7024  f1mpt  7207  isores3  7281  caofrss  7661  caoftrn  7663  sorpssuni  7677  sorpssint  7678  onint  7735  xpord3inddlem  8096  smogt  8299  fisupg  9188  ixpfi2  9250  fissuni  9257  indexfi  9260  fiinfg  9404  wemaplem2  9452  rankonidlem  9740  ac5num  9946  acni2  9956  acndom2  9964  alephle  9998  dfac5  10039  cfsmolem  10180  isf34lem7  10289  isf34lem6  10290  fin1a2s  10324  acncc  10350  ttukeylem6  10424  fpwwe2lem7  10548  gchina  10610  inar1  10686  tskord  10691  grudomon  10728  grur1a  10730  dedekind  11296  fimaxre  12086  fiminre  12089  uzwo  12824  xrsupsslem  13222  xrinfmsslem  13223  fsuppmapnn0fiub0  13916  rexanre  15270  rexuz3  15272  rexico  15277  cau3lem  15278  limsupval2  15403  rlim2lt  15420  rlim3  15421  lo1bdd2  15447  lo1bddrp  15448  o1lo1  15460  climrlim2  15470  2clim  15495  o1co  15509  rlimcn1  15511  rlimcn3  15513  climcn1  15515  climcn2  15516  subcn2  15518  o1of2  15536  rlimo1  15540  o1rlimmul  15542  lo1add  15550  lo1mul  15551  climsqz  15564  climsqz2  15565  rlimsqzlem  15572  lo1le  15575  climbdd  15595  caucvgrlem  15596  caucvgrlem2  15598  caurcvg2  15601  iseralt  15608  cvgcmp  15739  cvgcmpce  15741  gcdcllem1  16426  absproddvds  16544  coprmprod  16588  coprmproddvdslem  16589  pcfac  16827  pockthg  16834  infpnlem1  16838  prmreclem2  16845  prmreclem3  16846  vdwlem11  16919  vdwlem13  16921  vdwnnlem3  16925  isacs2  17576  acsfn1  17584  acsfn2  17586  catpropd  17632  drsdirfi  18228  ipodrsima  18464  isacs5  18471  mrelatglb  18483  mrelatlub  18485  isgrpinv  18923  dfgrp3e  18970  issubg4  19075  gsmsymgreqlem2  19360  finodsubmsubg  19496  gexdvds  19513  gexcl3  19516  sylow2blem3  19551  cyggeninv  19812  gsummptnn0fz  19915  dprdff  19943  issubdrg  20713  acsfn1p  20732  cygznlem3  21524  psdmul  22109  mptcoe1fsupp  22156  cply1coe0bi  22246  gsummoncoe1  22252  evls1fpws  22313  scmatdmat  22459  mdetdiagid  22544  mdetunilem9  22564  cpmatmcllem  22662  m2cpminvid2lem  22698  decpmatmulsumfsupp  22717  pmatcollpw1lem1  22718  pmatcollpw2lem  22721  pmatcollpwfi  22726  pm2mpf1  22743  mptcoe1matfsupp  22746  mp2pm2mplem4  22753  pm2mpmhmlem1  22762  pm2mp  22769  chpdmat  22785  chpscmat  22786  cpmidpmatlem3  22816  cayhamlem4  22832  neiptopnei  23076  cncnp  23224  isnrm2  23302  isreg2  23321  2ndcdisj  23400  islly2  23428  dislly  23441  kgen2ss  23499  ptbasfi  23525  ptclsg  23559  prdstopn  23572  txtube  23584  txlm  23592  isr0  23681  filuni  23829  alexsubALTlem3  23993  ptcmplem3  23998  ptcmplem4  23999  tsmsxplem1  24097  prdsmet  24314  metequiv2  24454  metcnpi3  24490  nmoleub  24675  rescncf  24846  cncfco  24856  evth  24914  lebnumlem3  24918  xlebnum  24920  nmoleub2lem2  25072  nmhmcn  25076  lmmcvg  25217  cmetcaulem  25244  caubl  25264  bcth3  25287  ovollb2lem  25445  ovoliunlem2  25460  ovolicc2lem3  25476  ovolicc2lem4  25477  nulmbl2  25493  volsup  25513  ioombl1lem4  25518  dyadmax  25555  vitalilem2  25566  vitalilem5  25569  mbfi1flimlem  25679  itg2seq  25699  itg2addlem  25715  itgcn  25802  limciun  25851  rolle  25950  dvfsumrlim  25994  itgsubst  26012  aannenlem1  26292  aalioulem3  26298  ulmcaulem  26359  ulmcau  26360  ulmss  26362  ulmbdd  26363  ulmcn  26364  ulmdvlem3  26367  mtest  26369  iblulm  26372  itgulm  26373  rlimcnp  26931  xrlimcnp  26934  rlimcxp  26940  o1cxp  26941  amgm  26957  lgambdd  27003  ftalem2  27040  isppw2  27081  mumullem2  27146  2sqlem6  27390  chtppilimlem2  27441  chtppilim  27442  pntrsumbnd2  27534  pntlem3  27576  nosupbnd1lem5  27680  noinfbnd1lem5  27695  noetasuplem4  27704  noetainflem4  27708  negbdaylem  28052  mulsuniflem  28145  elreno2  28491  isperp2  28787  axeuclidlem  29035  axeuclid  29036  uhgrnbgr0nb  29427  vtxdginducedm1fi  29618  cusgrrusgr  29655  rusgrpropnb  29657  rusgrpropedg  29658  rusgrpropadjvtx  29659  upgrewlkle2  29680  wlkvtxiedg  29698  upgrwlkvtxedg  29718  uspgr2wlkeq  29719  redwlk  29744  wlkdlem2  29755  lfgrwlkprop  29759  2pthnloop  29804  upgr2pthnlp  29805  pthdlem1  29839  pthdlem2lem  29840  wlkiswwlks1  29940  wlkiswwlks2lem4  29945  wwlksm1edg  29954  wwlksnred  29965  clwwlkccatlem  30064  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  cusconngr  30266  eucrctshift  30318  2pthfrgr  30359  3cyclfrgr  30363  nmoub3i  30848  ubthlem1  30945  ubthlem3  30947  ocsh  31358  chintcli  31406  chscllem2  31713  nmopub2tALT  31984  nmfnleub2  32001  lnconi  32108  riesz1  32140  rnbra  32182  leopadd  32207  leopmuli  32208  leoptr  32212  dmdbr3  32380  dmdbr4  32381  dmdbr5  32383  mdsl0  32385  mdsymlem6  32483  cdj1i  32508  acunirnmpt  32737  xrge0infss  32840  isdrng4  33377  elrspunidl  33509  cmppcmp  34015  zarclsiin  34028  lmxrge0  34109  ftc2re  34755  cvmlift2lem12  35508  opnrebl2  36515  neibastop1  36553  neibastop2lem  36554  neibastop3  36556  finixpnum  37806  lindsenlbs  37816  matunitlindflem1  37817  matunitlindflem2  37818  ptrecube  37821  poimirlem26  37847  poimirlem27  37848  poimirlem29  37850  poimirlem30  37851  poimir  37854  heicant  37856  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  filbcmb  37941  nninfnub  37952  geomcau  37960  sstotbnd2  37975  isbndx  37983  prdsbnd  37994  heibor1lem  38010  heiborlem1  38012  heibor  38022  rrncmslem  38033  intidl  38230  pclclN  40161  lauteq  40365  ltrnid  40405  mapdh9a  42059  primrootscoprmpow  42363  sticksstones3  42412  aks5lem5a  42455  aks5lem6  42456  fltaccoprm  42893  fltabcoprm  42895  flt4lem5  42903  elrfirn2  42948  isnacs3  42962  rencldnfilem  43072  kelac1  43315  naddgeoa  43646  neik0pk1imk0  44298  cvgdvgrat  44564  neglimc  45901  limsupub  45958  limsuppnflem  45964  limsupre3lem  45986  limsupvaluz2  45992  supcnvlimsup  45994  climuzlem  45997  liminfval2  46022  limsupgtlem  46031  liminflelimsupuz  46039  liminflimsupclim  46061  xlimpnfxnegmnf  46068  liminflimsupxrre  46071  xlimmnfv  46088  xlimpnfv  46092  stoweidlem7  46261  fourierdlem73  46433  sge0isum  46681  meaiuninc3v  46738  preimageiingt  46974  preimaleiinlt  46975  smflimlem3  47027  smflimlem4  47028  cfsetsnfsetfo  47316  2reu8i  47369  iccpartres  47674  uhgrimisgrgric  48187  grlictr  48271  clnbgr3stgrgrlim  48275  clnbgr3stgrgrlic  48276  upwlkwlk  48395  upgrwlkupwlk  48396  copisnmnd  48425  2zrngnmlid2  48513  ply1mulgsumlem1  48642  ply1mulgsumlem3  48644  ply1mulgsumlem4  48645  snlindsntor  48727  eenglngeehlnmlem1  48993  eenglngeehlnmlem2  48994  iinfsubc  49313