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 2114  ∀wral 3138

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 209  df-an 399  df-ral 3143

This theorem is referenced by:  ralimdv  3178  ralimdvva  3179  wereu2  5552  fveqressseq  6847  f1mpt  7019  isores3  7088  caofrss  7442  caoftrn  7444  sorpssuni  7458  sorpssint  7459  onint  7510  smogt  8004  fisupg  8766  ixpfi2  8822  fissuni  8829  indexfi  8832  fiinfg  8963  wemaplem2  9011  rankonidlem  9257  ac5num  9462  acni2  9472  acndom2  9480  alephle  9514  dfac5  9554  cfsmolem  9692  isf34lem7  9801  isf34lem6  9802  fin1a2s  9836  acncc  9862  ttukeylem6  9936  fpwwe2lem8  10059  gchina  10121  inar1  10197  tskord  10202  grudomon  10239  grur1a  10241  dedekind  10803  fimaxre  11584  fimaxreOLD  11585  fiminre  11588  uzwo  12312  xrsupsslem  12701  xrinfmsslem  12702  fsuppmapnn0fiub0  13362  rexanre  14706  rexuz3  14708  rexico  14713  cau3lem  14714  limsupval2  14837  rlim2lt  14854  rlim3  14855  lo1bdd2  14881  lo1bddrp  14882  o1lo1  14894  climrlim2  14904  2clim  14929  o1co  14943  rlimcn1  14945  rlimcn2  14947  climcn1  14948  climcn2  14949  subcn2  14951  o1of2  14969  rlimo1  14973  o1rlimmul  14975  lo1add  14983  lo1mul  14984  climsqz  14997  climsqz2  14998  rlimsqzlem  15005  lo1le  15008  climbdd  15028  caucvgrlem  15029  caucvgrlem2  15031  caurcvg2  15034  iseralt  15041  cvgcmp  15171  cvgcmpce  15173  gcdcllem1  15848  absproddvds  15961  coprmprod  16005  coprmproddvdslem  16006  pcfac  16235  pockthg  16242  infpnlem1  16246  prmreclem2  16253  prmreclem3  16254  vdwlem11  16327  vdwlem13  16329  vdwnnlem3  16333  isacs2  16924  acsfn1  16932  acsfn2  16934  catpropd  16979  drsdirfi  17548  ipodrsima  17775  isacs5  17782  mrelatglb  17794  mrelatlub  17796  isgrpinv  18156  dfgrp3e  18199  issubg4  18298  gsmsymgreqlem2  18559  gexdvds  18709  gexcl3  18712  sylow2blem3  18747  cyggeninv  19002  gsummptnn0fz  19106  dprdff  19134  issubdrg  19560  acsfn1p  19578  mptcoe1fsupp  20383  cply1coe0bi  20468  gsummoncoe1  20472  cygznlem3  20716  scmatdmat  21124  mdetdiagid  21209  mdetunilem9  21229  cpmatmcllem  21326  m2cpminvid2lem  21362  decpmatmulsumfsupp  21381  pmatcollpw1lem1  21382  pmatcollpw2lem  21385  pmatcollpwfi  21390  pm2mpf1  21407  mptcoe1matfsupp  21410  mp2pm2mplem4  21417  pm2mpmhmlem1  21426  pm2mp  21433  chpdmat  21449  chpscmat  21450  cpmidpmatlem3  21480  cayhamlem4  21496  neiptopnei  21740  cncnp  21888  isnrm2  21966  isreg2  21985  2ndcdisj  22064  islly2  22092  dislly  22105  kgen2ss  22163  ptbasfi  22189  ptclsg  22223  prdstopn  22236  txtube  22248  txlm  22256  isr0  22345  filuni  22493  alexsubALTlem3  22657  ptcmplem3  22662  ptcmplem4  22663  tsmsxplem1  22761  prdsmet  22980  metequiv2  23120  metcnpi3  23156  nmoleub  23340  rescncf  23505  cncfco  23515  evth  23563  lebnumlem3  23567  xlebnum  23569  nmoleub2lem2  23720  nmhmcn  23724  lmmcvg  23864  cmetcaulem  23891  caubl  23911  bcth3  23934  ovollb2lem  24089  ovoliunlem2  24104  ovolicc2lem3  24120  ovolicc2lem4  24121  nulmbl2  24137  volsup  24157  ioombl1lem4  24162  dyadmax  24199  vitalilem2  24210  vitalilem5  24213  mbfi1flimlem  24323  itg2seq  24343  itg2addlem  24359  itgcn  24443  limciun  24492  rolle  24587  dvfsumrlim  24628  itgsubst  24646  aannenlem1  24917  aalioulem3  24923  ulmcaulem  24982  ulmcau  24983  ulmss  24985  ulmbdd  24986  ulmcn  24987  ulmdvlem3  24990  mtest  24992  iblulm  24995  itgulm  24996  rlimcnp  25543  xrlimcnp  25546  rlimcxp  25551  o1cxp  25552  amgm  25568  lgambdd  25614  ftalem2  25651  isppw2  25692  mumullem2  25757  2sqlem6  25999  chtppilimlem2  26050  chtppilim  26051  pntrsumbnd2  26143  pntlem3  26185  isperp2  26501  axeuclidlem  26748  axeuclid  26749  uhgrnbgr0nb  27136  vtxdginducedm1fi  27326  cusgrrusgr  27363  rusgrpropnb  27365  rusgrpropedg  27366  rusgrpropadjvtx  27367  upgrewlkle2  27388  wlkvtxiedg  27406  upgrwlkvtxedg  27426  uspgr2wlkeq  27427  redwlk  27454  wlkdlem2  27465  lfgrwlkprop  27469  2pthnloop  27512  upgr2pthnlp  27513  pthdlem1  27547  pthdlem2lem  27548  wlkiswwlks1  27645  wlkiswwlks2lem4  27650  wwlksm1edg  27659  wwlksnred  27670  clwwlkccatlem  27767  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  cusconngr  27970  eucrctshift  28022  2pthfrgr  28063  3cyclfrgr  28067  nmoub3i  28550  ubthlem1  28647  ubthlem3  28649  ocsh  29060  chintcli  29108  chscllem2  29415  nmopub2tALT  29686  nmfnleub2  29703  lnconi  29810  riesz1  29842  rnbra  29884  leopadd  29909  leopmuli  29910  leoptr  29914  dmdbr3  30082  dmdbr4  30083  dmdbr5  30085  mdsl0  30087  mdsymlem6  30185  cdj1i  30210  acunirnmpt  30404  xrge0infss  30484  cmppcmp  31122  lmxrge0  31195  ftc2re  31869  cvmlift2lem12  32561  frpomin  33078  nosupbnd1lem5  33212  noetalem3  33219  opnrebl2  33669  neibastop1  33707  neibastop2lem  33708  neibastop3  33710  finixpnum  34892  lindsenlbs  34902  matunitlindflem1  34903  matunitlindflem2  34904  ptrecube  34907  poimirlem26  34933  poimirlem27  34934  poimirlem29  34936  poimirlem30  34937  poimir  34940  heicant  34942  itg2addnclem  34958  itg2addnclem3  34960  itg2addnc  34961  filbcmb  35030  nninfnub  35041  geomcau  35049  sstotbnd2  35067  isbndx  35075  prdsbnd  35086  heibor1lem  35102  heiborlem1  35104  heibor  35114  rrncmslem  35125  intidl  35322  pclclN  37042  lauteq  37246  ltrnid  37286  mapdh9a  38940  elrfirn2  39313  isnacs3  39327  rencldnfilem  39437  kelac1  39683  neik0pk1imk0  40417  cvgdvgrat  40665  neglimc  41948  limsupub  42005  limsuppnflem  42011  limsupre3lem  42033  limsupvaluz2  42039  supcnvlimsup  42041  climuzlem  42044  liminfval2  42069  limsupgtlem  42078  liminflelimsupuz  42086  liminflimsupclim  42108  xlimpnfxnegmnf  42115  liminflimsupxrre  42118  xlimmnfv  42135  xlimpnfv  42139  stoweidlem7  42312  fourierdlem73  42484  sge0isum  42729  meaiuninc3v  42786  preimageiingt  43018  preimaleiinlt  43019  smflimlem3  43069  smflimlem4  43070  2reu8i  43332  iccpartres  43598  upwlkwlk  44034  upgrwlkupwlk  44035  copisnmnd  44096  2zrngnmlid2  44242  ply1mulgsumlem1  44460  ply1mulgsumlem3  44462  ply1mulgsumlem4  44463  snlindsntor  44546  eenglngeehlnmlem1  44744  eenglngeehlnmlem2  44745