Theorem ralimdva 3167

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  ralimdv  3169  ralimdvva  3206  wereu2  5682  frpomin  6361  fveqressseq  7099  f1mpt  7281  isores3  7355  caofrss  7736  caoftrn  7738  sorpssuni  7752  sorpssint  7753  onint  7810  xpord3inddlem  8179  smogt  8407  fisupg  9324  ixpfi2  9390  fissuni  9397  indexfi  9400  fiinfg  9539  wemaplem2  9587  rankonidlem  9868  ac5num  10076  acni2  10086  acndom2  10094  alephle  10128  dfac5  10169  cfsmolem  10310  isf34lem7  10419  isf34lem6  10420  fin1a2s  10454  acncc  10480  ttukeylem6  10554  fpwwe2lem7  10677  gchina  10739  inar1  10815  tskord  10820  grudomon  10857  grur1a  10859  dedekind  11424  fimaxre  12212  fiminre  12215  uzwo  12953  xrsupsslem  13349  xrinfmsslem  13350  fsuppmapnn0fiub0  14034  rexanre  15385  rexuz3  15387  rexico  15392  cau3lem  15393  limsupval2  15516  rlim2lt  15533  rlim3  15534  lo1bdd2  15560  lo1bddrp  15561  o1lo1  15573  climrlim2  15583  2clim  15608  o1co  15622  rlimcn1  15624  rlimcn3  15626  climcn1  15628  climcn2  15629  subcn2  15631  o1of2  15649  rlimo1  15653  o1rlimmul  15655  lo1add  15663  lo1mul  15664  climsqz  15677  climsqz2  15678  rlimsqzlem  15685  lo1le  15688  climbdd  15708  caucvgrlem  15709  caucvgrlem2  15711  caurcvg2  15714  iseralt  15721  cvgcmp  15852  cvgcmpce  15854  gcdcllem1  16536  absproddvds  16654  coprmprod  16698  coprmproddvdslem  16699  pcfac  16937  pockthg  16944  infpnlem1  16948  prmreclem2  16955  prmreclem3  16956  vdwlem11  17029  vdwlem13  17031  vdwnnlem3  17035  isacs2  17696  acsfn1  17704  acsfn2  17706  catpropd  17752  drsdirfi  18351  ipodrsima  18586  isacs5  18593  mrelatglb  18605  mrelatlub  18607  isgrpinv  19011  dfgrp3e  19058  issubg4  19163  gsmsymgreqlem2  19449  finodsubmsubg  19585  gexdvds  19602  gexcl3  19605  sylow2blem3  19640  cyggeninv  19901  gsummptnn0fz  20004  dprdff  20032  issubdrg  20781  acsfn1p  20800  cygznlem3  21588  psdmul  22170  mptcoe1fsupp  22217  cply1coe0bi  22306  gsummoncoe1  22312  evls1fpws  22373  scmatdmat  22521  mdetdiagid  22606  mdetunilem9  22626  cpmatmcllem  22724  m2cpminvid2lem  22760  decpmatmulsumfsupp  22779  pmatcollpw1lem1  22780  pmatcollpw2lem  22783  pmatcollpwfi  22788  pm2mpf1  22805  mptcoe1matfsupp  22808  mp2pm2mplem4  22815  pm2mpmhmlem1  22824  pm2mp  22831  chpdmat  22847  chpscmat  22848  cpmidpmatlem3  22878  cayhamlem4  22894  neiptopnei  23140  cncnp  23288  isnrm2  23366  isreg2  23385  2ndcdisj  23464  islly2  23492  dislly  23505  kgen2ss  23563  ptbasfi  23589  ptclsg  23623  prdstopn  23636  txtube  23648  txlm  23656  isr0  23745  filuni  23893  alexsubALTlem3  24057  ptcmplem3  24062  ptcmplem4  24063  tsmsxplem1  24161  prdsmet  24380  metequiv2  24523  metcnpi3  24559  nmoleub  24752  rescncf  24923  cncfco  24933  evth  24991  lebnumlem3  24995  xlebnum  24997  nmoleub2lem2  25149  nmhmcn  25153  lmmcvg  25295  cmetcaulem  25322  caubl  25342  bcth3  25365  ovollb2lem  25523  ovoliunlem2  25538  ovolicc2lem3  25554  ovolicc2lem4  25555  nulmbl2  25571  volsup  25591  ioombl1lem4  25596  dyadmax  25633  vitalilem2  25644  vitalilem5  25647  mbfi1flimlem  25757  itg2seq  25777  itg2addlem  25793  itgcn  25880  limciun  25929  rolle  26028  dvfsumrlim  26072  itgsubst  26090  aannenlem1  26370  aalioulem3  26376  ulmcaulem  26437  ulmcau  26438  ulmss  26440  ulmbdd  26441  ulmcn  26442  ulmdvlem3  26445  mtest  26447  iblulm  26450  itgulm  26451  rlimcnp  27008  xrlimcnp  27011  rlimcxp  27017  o1cxp  27018  amgm  27034  lgambdd  27080  ftalem2  27117  isppw2  27158  mumullem2  27223  2sqlem6  27467  chtppilimlem2  27518  chtppilim  27519  pntrsumbnd2  27611  pntlem3  27653  nosupbnd1lem5  27757  noinfbnd1lem5  27772  noetasuplem4  27781  noetainflem4  27785  negsbdaylem  28088  mulsuniflem  28175  isperp2  28723  axeuclidlem  28977  axeuclid  28978  uhgrnbgr0nb  29371  vtxdginducedm1fi  29562  cusgrrusgr  29599  rusgrpropnb  29601  rusgrpropedg  29602  rusgrpropadjvtx  29603  upgrewlkle2  29624  wlkvtxiedg  29643  upgrwlkvtxedg  29663  uspgr2wlkeq  29664  redwlk  29690  wlkdlem2  29701  lfgrwlkprop  29705  2pthnloop  29751  upgr2pthnlp  29752  pthdlem1  29786  pthdlem2lem  29787  wlkiswwlks1  29887  wlkiswwlks2lem4  29892  wwlksm1edg  29901  wwlksnred  29912  clwwlkccatlem  30008  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  cusconngr  30210  eucrctshift  30262  2pthfrgr  30303  3cyclfrgr  30307  nmoub3i  30792  ubthlem1  30889  ubthlem3  30891  ocsh  31302  chintcli  31350  chscllem2  31657  nmopub2tALT  31928  nmfnleub2  31945  lnconi  32052  riesz1  32084  rnbra  32126  leopadd  32151  leopmuli  32152  leoptr  32156  dmdbr3  32324  dmdbr4  32325  dmdbr5  32327  mdsl0  32329  mdsymlem6  32427  cdj1i  32452  acunirnmpt  32669  xrge0infss  32764  isdrng4  33298  elrspunidl  33456  cmppcmp  33857  zarclsiin  33870  lmxrge0  33951  ftc2re  34613  cvmlift2lem12  35319  opnrebl2  36322  neibastop1  36360  neibastop2lem  36361  neibastop3  36363  finixpnum  37612  lindsenlbs  37622  matunitlindflem1  37623  matunitlindflem2  37624  ptrecube  37627  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  poimirlem30  37657  poimir  37660  heicant  37662  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  filbcmb  37747  nninfnub  37758  geomcau  37766  sstotbnd2  37781  isbndx  37789  prdsbnd  37800  heibor1lem  37816  heiborlem1  37818  heibor  37828  rrncmslem  37839  intidl  38036  pclclN  39893  lauteq  40097  ltrnid  40137  mapdh9a  41791  primrootscoprmpow  42100  sticksstones3  42149  aks5lem5a  42192  aks5lem6  42193  fltaccoprm  42650  fltabcoprm  42652  flt4lem5  42660  elrfirn2  42707  isnacs3  42721  rencldnfilem  42831  kelac1  43075  naddgeoa  43407  neik0pk1imk0  44060  cvgdvgrat  44332  neglimc  45662  limsupub  45719  limsuppnflem  45725  limsupre3lem  45747  limsupvaluz2  45753  supcnvlimsup  45755  climuzlem  45758  liminfval2  45783  limsupgtlem  45792  liminflelimsupuz  45800  liminflimsupclim  45822  xlimpnfxnegmnf  45829  liminflimsupxrre  45832  xlimmnfv  45849  xlimpnfv  45853  stoweidlem7  46022  fourierdlem73  46194  sge0isum  46442  meaiuninc3v  46499  preimageiingt  46735  preimaleiinlt  46736  smflimlem3  46788  smflimlem4  46789  cfsetsnfsetfo  47072  2reu8i  47125  iccpartres  47405  uhgrimisgrgric  47899  grlictr  47975  clnbgr3stgrgrlic  47979  upwlkwlk  48055  upgrwlkupwlk  48056  copisnmnd  48085  2zrngnmlid2  48173  ply1mulgsumlem1  48303  ply1mulgsumlem3  48305  ply1mulgsumlem4  48306  snlindsntor  48388  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659