Theorem ralimdva 3164

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∀wral 3058

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

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

This theorem is referenced by:  ralimdv  3166  ralimdvva  3203  wereu2  5685  frpomin  6362  fveqressseq  7098  f1mpt  7280  isores3  7354  caofrss  7734  caoftrn  7736  sorpssuni  7750  sorpssint  7751  onint  7809  xpord3inddlem  8177  smogt  8405  fisupg  9321  ixpfi2  9387  fissuni  9394  indexfi  9397  fiinfg  9536  wemaplem2  9584  rankonidlem  9865  ac5num  10073  acni2  10083  acndom2  10091  alephle  10125  dfac5  10166  cfsmolem  10307  isf34lem7  10416  isf34lem6  10417  fin1a2s  10451  acncc  10477  ttukeylem6  10551  fpwwe2lem7  10674  gchina  10736  inar1  10812  tskord  10817  grudomon  10854  grur1a  10856  dedekind  11421  fimaxre  12209  fiminre  12212  uzwo  12950  xrsupsslem  13345  xrinfmsslem  13346  fsuppmapnn0fiub0  14030  rexanre  15381  rexuz3  15383  rexico  15388  cau3lem  15389  limsupval2  15512  rlim2lt  15529  rlim3  15530  lo1bdd2  15556  lo1bddrp  15557  o1lo1  15569  climrlim2  15579  2clim  15604  o1co  15618  rlimcn1  15620  rlimcn3  15622  climcn1  15624  climcn2  15625  subcn2  15627  o1of2  15645  rlimo1  15649  o1rlimmul  15651  lo1add  15659  lo1mul  15660  climsqz  15673  climsqz2  15674  rlimsqzlem  15681  lo1le  15684  climbdd  15704  caucvgrlem  15705  caucvgrlem2  15707  caurcvg2  15710  iseralt  15717  cvgcmp  15848  cvgcmpce  15850  gcdcllem1  16532  absproddvds  16650  coprmprod  16694  coprmproddvdslem  16695  pcfac  16932  pockthg  16939  infpnlem1  16943  prmreclem2  16950  prmreclem3  16951  vdwlem11  17024  vdwlem13  17026  vdwnnlem3  17030  isacs2  17697  acsfn1  17705  acsfn2  17707  catpropd  17753  drsdirfi  18362  ipodrsima  18598  isacs5  18605  mrelatglb  18617  mrelatlub  18619  isgrpinv  19023  dfgrp3e  19070  issubg4  19175  gsmsymgreqlem2  19463  finodsubmsubg  19599  gexdvds  19616  gexcl3  19619  sylow2blem3  19654  cyggeninv  19915  gsummptnn0fz  20018  dprdff  20046  issubdrg  20797  acsfn1p  20816  cygznlem3  21605  psdmul  22187  mptcoe1fsupp  22232  cply1coe0bi  22321  gsummoncoe1  22327  evls1fpws  22388  scmatdmat  22536  mdetdiagid  22621  mdetunilem9  22641  cpmatmcllem  22739  m2cpminvid2lem  22775  decpmatmulsumfsupp  22794  pmatcollpw1lem1  22795  pmatcollpw2lem  22798  pmatcollpwfi  22803  pm2mpf1  22820  mptcoe1matfsupp  22823  mp2pm2mplem4  22830  pm2mpmhmlem1  22839  pm2mp  22846  chpdmat  22862  chpscmat  22863  cpmidpmatlem3  22893  cayhamlem4  22909  neiptopnei  23155  cncnp  23303  isnrm2  23381  isreg2  23400  2ndcdisj  23479  islly2  23507  dislly  23520  kgen2ss  23578  ptbasfi  23604  ptclsg  23638  prdstopn  23651  txtube  23663  txlm  23671  isr0  23760  filuni  23908  alexsubALTlem3  24072  ptcmplem3  24077  ptcmplem4  24078  tsmsxplem1  24176  prdsmet  24395  metequiv2  24538  metcnpi3  24574  nmoleub  24767  rescncf  24936  cncfco  24946  evth  25004  lebnumlem3  25008  xlebnum  25010  nmoleub2lem2  25162  nmhmcn  25166  lmmcvg  25308  cmetcaulem  25335  caubl  25355  bcth3  25378  ovollb2lem  25536  ovoliunlem2  25551  ovolicc2lem3  25567  ovolicc2lem4  25568  nulmbl2  25584  volsup  25604  ioombl1lem4  25609  dyadmax  25646  vitalilem2  25657  vitalilem5  25660  mbfi1flimlem  25771  itg2seq  25791  itg2addlem  25807  itgcn  25894  limciun  25943  rolle  26042  dvfsumrlim  26086  itgsubst  26104  aannenlem1  26384  aalioulem3  26390  ulmcaulem  26451  ulmcau  26452  ulmss  26454  ulmbdd  26455  ulmcn  26456  ulmdvlem3  26459  mtest  26461  iblulm  26464  itgulm  26465  rlimcnp  27022  xrlimcnp  27025  rlimcxp  27031  o1cxp  27032  amgm  27048  lgambdd  27094  ftalem2  27131  isppw2  27172  mumullem2  27237  2sqlem6  27481  chtppilimlem2  27532  chtppilim  27533  pntrsumbnd2  27625  pntlem3  27667  nosupbnd1lem5  27771  noinfbnd1lem5  27786  noetasuplem4  27795  noetainflem4  27799  negsbdaylem  28102  mulsuniflem  28189  isperp2  28737  axeuclidlem  28991  axeuclid  28992  uhgrnbgr0nb  29385  vtxdginducedm1fi  29576  cusgrrusgr  29613  rusgrpropnb  29615  rusgrpropedg  29616  rusgrpropadjvtx  29617  upgrewlkle2  29638  wlkvtxiedg  29657  upgrwlkvtxedg  29677  uspgr2wlkeq  29678  redwlk  29704  wlkdlem2  29715  lfgrwlkprop  29719  2pthnloop  29763  upgr2pthnlp  29764  pthdlem1  29798  pthdlem2lem  29799  wlkiswwlks1  29896  wlkiswwlks2lem4  29901  wwlksm1edg  29910  wwlksnred  29921  clwwlkccatlem  30017  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  cusconngr  30219  eucrctshift  30271  2pthfrgr  30312  3cyclfrgr  30316  nmoub3i  30801  ubthlem1  30898  ubthlem3  30900  ocsh  31311  chintcli  31359  chscllem2  31666  nmopub2tALT  31937  nmfnleub2  31954  lnconi  32061  riesz1  32093  rnbra  32135  leopadd  32160  leopmuli  32161  leoptr  32165  dmdbr3  32333  dmdbr4  32334  dmdbr5  32336  mdsl0  32338  mdsymlem6  32436  cdj1i  32461  acunirnmpt  32675  xrge0infss  32770  isdrng4  33278  elrspunidl  33435  cmppcmp  33818  zarclsiin  33831  lmxrge0  33912  ftc2re  34591  cvmlift2lem12  35298  opnrebl2  36303  neibastop1  36341  neibastop2lem  36342  neibastop3  36344  finixpnum  37591  lindsenlbs  37601  matunitlindflem1  37602  matunitlindflem2  37603  ptrecube  37606  poimirlem26  37632  poimirlem27  37633  poimirlem29  37635  poimirlem30  37636  poimir  37639  heicant  37641  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  filbcmb  37726  nninfnub  37737  geomcau  37745  sstotbnd2  37760  isbndx  37768  prdsbnd  37779  heibor1lem  37795  heiborlem1  37797  heibor  37807  rrncmslem  37818  intidl  38015  pclclN  39873  lauteq  40077  ltrnid  40117  mapdh9a  41771  primrootscoprmpow  42080  sticksstones3  42129  aks5lem5a  42172  aks5lem6  42173  fltaccoprm  42626  fltabcoprm  42628  flt4lem5  42636  elrfirn2  42683  isnacs3  42697  rencldnfilem  42807  kelac1  43051  naddgeoa  43383  neik0pk1imk0  44036  cvgdvgrat  44308  neglimc  45602  limsupub  45659  limsuppnflem  45665  limsupre3lem  45687  limsupvaluz2  45693  supcnvlimsup  45695  climuzlem  45698  liminfval2  45723  limsupgtlem  45732  liminflelimsupuz  45740  liminflimsupclim  45762  xlimpnfxnegmnf  45769  liminflimsupxrre  45772  xlimmnfv  45789  xlimpnfv  45793  stoweidlem7  45962  fourierdlem73  46134  sge0isum  46382  meaiuninc3v  46439  preimageiingt  46675  preimaleiinlt  46676  smflimlem3  46728  smflimlem4  46729  cfsetsnfsetfo  47009  2reu8i  47062  iccpartres  47342  uhgrimisgrgric  47836  grlictr  47910  clnbgr3stgrgrlic  47914  upwlkwlk  47982  upgrwlkupwlk  47983  copisnmnd  48012  2zrngnmlid2  48100  ply1mulgsumlem1  48231  ply1mulgsumlem3  48233  ply1mulgsumlem4  48234  snlindsntor  48316  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587