Theorem ralimdva 3146

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3045

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 3046

This theorem is referenced by:  ralimdv  3148  ralimdvva  3185  wereu2  5638  frpomin  6316  fveqressseq  7054  f1mpt  7239  isores3  7313  caofrss  7695  caoftrn  7697  sorpssuni  7711  sorpssint  7712  onint  7769  xpord3inddlem  8136  smogt  8339  fisupg  9242  ixpfi2  9308  fissuni  9315  indexfi  9318  fiinfg  9459  wemaplem2  9507  rankonidlem  9788  ac5num  9996  acni2  10006  acndom2  10014  alephle  10048  dfac5  10089  cfsmolem  10230  isf34lem7  10339  isf34lem6  10340  fin1a2s  10374  acncc  10400  ttukeylem6  10474  fpwwe2lem7  10597  gchina  10659  inar1  10735  tskord  10740  grudomon  10777  grur1a  10779  dedekind  11344  fimaxre  12134  fiminre  12137  uzwo  12877  xrsupsslem  13274  xrinfmsslem  13275  fsuppmapnn0fiub0  13965  rexanre  15320  rexuz3  15322  rexico  15327  cau3lem  15328  limsupval2  15453  rlim2lt  15470  rlim3  15471  lo1bdd2  15497  lo1bddrp  15498  o1lo1  15510  climrlim2  15520  2clim  15545  o1co  15559  rlimcn1  15561  rlimcn3  15563  climcn1  15565  climcn2  15566  subcn2  15568  o1of2  15586  rlimo1  15590  o1rlimmul  15592  lo1add  15600  lo1mul  15601  climsqz  15614  climsqz2  15615  rlimsqzlem  15622  lo1le  15625  climbdd  15645  caucvgrlem  15646  caucvgrlem2  15648  caurcvg2  15651  iseralt  15658  cvgcmp  15789  cvgcmpce  15791  gcdcllem1  16476  absproddvds  16594  coprmprod  16638  coprmproddvdslem  16639  pcfac  16877  pockthg  16884  infpnlem1  16888  prmreclem2  16895  prmreclem3  16896  vdwlem11  16969  vdwlem13  16971  vdwnnlem3  16975  isacs2  17621  acsfn1  17629  acsfn2  17631  catpropd  17677  drsdirfi  18273  ipodrsima  18507  isacs5  18514  mrelatglb  18526  mrelatlub  18528  isgrpinv  18932  dfgrp3e  18979  issubg4  19084  gsmsymgreqlem2  19368  finodsubmsubg  19504  gexdvds  19521  gexcl3  19524  sylow2blem3  19559  cyggeninv  19820  gsummptnn0fz  19923  dprdff  19951  issubdrg  20696  acsfn1p  20715  cygznlem3  21486  psdmul  22060  mptcoe1fsupp  22107  cply1coe0bi  22196  gsummoncoe1  22202  evls1fpws  22263  scmatdmat  22409  mdetdiagid  22494  mdetunilem9  22514  cpmatmcllem  22612  m2cpminvid2lem  22648  decpmatmulsumfsupp  22667  pmatcollpw1lem1  22668  pmatcollpw2lem  22671  pmatcollpwfi  22676  pm2mpf1  22693  mptcoe1matfsupp  22696  mp2pm2mplem4  22703  pm2mpmhmlem1  22712  pm2mp  22719  chpdmat  22735  chpscmat  22736  cpmidpmatlem3  22766  cayhamlem4  22782  neiptopnei  23026  cncnp  23174  isnrm2  23252  isreg2  23271  2ndcdisj  23350  islly2  23378  dislly  23391  kgen2ss  23449  ptbasfi  23475  ptclsg  23509  prdstopn  23522  txtube  23534  txlm  23542  isr0  23631  filuni  23779  alexsubALTlem3  23943  ptcmplem3  23948  ptcmplem4  23949  tsmsxplem1  24047  prdsmet  24265  metequiv2  24405  metcnpi3  24441  nmoleub  24626  rescncf  24797  cncfco  24807  evth  24865  lebnumlem3  24869  xlebnum  24871  nmoleub2lem2  25023  nmhmcn  25027  lmmcvg  25168  cmetcaulem  25195  caubl  25215  bcth3  25238  ovollb2lem  25396  ovoliunlem2  25411  ovolicc2lem3  25427  ovolicc2lem4  25428  nulmbl2  25444  volsup  25464  ioombl1lem4  25469  dyadmax  25506  vitalilem2  25517  vitalilem5  25520  mbfi1flimlem  25630  itg2seq  25650  itg2addlem  25666  itgcn  25753  limciun  25802  rolle  25901  dvfsumrlim  25945  itgsubst  25963  aannenlem1  26243  aalioulem3  26249  ulmcaulem  26310  ulmcau  26311  ulmss  26313  ulmbdd  26314  ulmcn  26315  ulmdvlem3  26318  mtest  26320  iblulm  26323  itgulm  26324  rlimcnp  26882  xrlimcnp  26885  rlimcxp  26891  o1cxp  26892  amgm  26908  lgambdd  26954  ftalem2  26991  isppw2  27032  mumullem2  27097  2sqlem6  27341  chtppilimlem2  27392  chtppilim  27393  pntrsumbnd2  27485  pntlem3  27527  nosupbnd1lem5  27631  noinfbnd1lem5  27646  noetasuplem4  27655  noetainflem4  27659  negsbdaylem  27969  mulsuniflem  28059  isperp2  28649  axeuclidlem  28896  axeuclid  28897  uhgrnbgr0nb  29288  vtxdginducedm1fi  29479  cusgrrusgr  29516  rusgrpropnb  29518  rusgrpropedg  29519  rusgrpropadjvtx  29520  upgrewlkle2  29541  wlkvtxiedg  29560  upgrwlkvtxedg  29580  uspgr2wlkeq  29581  redwlk  29607  wlkdlem2  29618  lfgrwlkprop  29622  2pthnloop  29668  upgr2pthnlp  29669  pthdlem1  29703  pthdlem2lem  29704  wlkiswwlks1  29804  wlkiswwlks2lem4  29809  wwlksm1edg  29818  wwlksnred  29829  clwwlkccatlem  29925  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  cusconngr  30127  eucrctshift  30179  2pthfrgr  30220  3cyclfrgr  30224  nmoub3i  30709  ubthlem1  30806  ubthlem3  30808  ocsh  31219  chintcli  31267  chscllem2  31574  nmopub2tALT  31845  nmfnleub2  31862  lnconi  31969  riesz1  32001  rnbra  32043  leopadd  32068  leopmuli  32069  leoptr  32073  dmdbr3  32241  dmdbr4  32242  dmdbr5  32244  mdsl0  32246  mdsymlem6  32344  cdj1i  32369  acunirnmpt  32590  xrge0infss  32690  isdrng4  33252  elrspunidl  33406  cmppcmp  33855  zarclsiin  33868  lmxrge0  33949  ftc2re  34596  cvmlift2lem12  35308  opnrebl2  36316  neibastop1  36354  neibastop2lem  36355  neibastop3  36357  finixpnum  37606  lindsenlbs  37616  matunitlindflem1  37617  matunitlindflem2  37618  ptrecube  37621  poimirlem26  37647  poimirlem27  37648  poimirlem29  37650  poimirlem30  37651  poimir  37654  heicant  37656  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  filbcmb  37741  nninfnub  37752  geomcau  37760  sstotbnd2  37775  isbndx  37783  prdsbnd  37794  heibor1lem  37810  heiborlem1  37812  heibor  37822  rrncmslem  37833  intidl  38030  pclclN  39892  lauteq  40096  ltrnid  40136  mapdh9a  41790  primrootscoprmpow  42094  sticksstones3  42143  aks5lem5a  42186  aks5lem6  42187  fltaccoprm  42635  fltabcoprm  42637  flt4lem5  42645  elrfirn2  42691  isnacs3  42705  rencldnfilem  42815  kelac1  43059  naddgeoa  43390  neik0pk1imk0  44043  cvgdvgrat  44309  neglimc  45652  limsupub  45709  limsuppnflem  45715  limsupre3lem  45737  limsupvaluz2  45743  supcnvlimsup  45745  climuzlem  45748  liminfval2  45773  limsupgtlem  45782  liminflelimsupuz  45790  liminflimsupclim  45812  xlimpnfxnegmnf  45819  liminflimsupxrre  45822  xlimmnfv  45839  xlimpnfv  45843  stoweidlem7  46012  fourierdlem73  46184  sge0isum  46432  meaiuninc3v  46489  preimageiingt  46725  preimaleiinlt  46726  smflimlem3  46778  smflimlem4  46779  cfsetsnfsetfo  47065  2reu8i  47118  iccpartres  47423  uhgrimisgrgric  47935  grlictr  48011  clnbgr3stgrgrlic  48015  upwlkwlk  48131  upgrwlkupwlk  48132  copisnmnd  48161  2zrngnmlid2  48249  ply1mulgsumlem1  48379  ply1mulgsumlem3  48381  ply1mulgsumlem4  48382  snlindsntor  48464  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  iinfsubc  49051