Theorem ralimdva 3151

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 413	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	a2d 29	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)))
4	3	ralimdv2 3148	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3054

This theorem is referenced by:  ralimdv  3153  ralimdvva  3186  wereu2  5615  frpomin  6291  fveqressseq  7020  f1mpt  7205  isores3  7279  caofrss  7659  caoftrn  7661  sorpssuni  7675  sorpssint  7676  onint  7733  xpord3inddlem  8094  smogt  8297  fisupg  9188  ixpfi2  9250  fissuni  9257  indexfi  9260  fiinfg  9404  wemaplem2  9452  rankonidlem  9743  ac5num  9949  acni2  9959  acndom2  9967  alephle  10001  dfac5  10042  cfsmolem  10183  isf34lem7  10292  isf34lem6  10293  fin1a2s  10327  acncc  10353  ttukeylem6  10427  fpwwe2lem7  10551  gchina  10613  inar1  10689  tskord  10694  grudomon  10731  grur1a  10733  dedekind  11300  fimaxre  12091  fiminre  12094  uzwo  12852  xrsupsslem  13250  xrinfmsslem  13251  fsuppmapnn0fiub0  13946  rexanre  15300  rexuz3  15302  rexico  15307  cau3lem  15308  limsupval2  15433  rlim2lt  15450  rlim3  15451  lo1bdd2  15477  lo1bddrp  15478  o1lo1  15490  climrlim2  15500  2clim  15525  o1co  15539  rlimcn1  15541  rlimcn3  15543  climcn1  15545  climcn2  15546  subcn2  15548  o1of2  15566  rlimo1  15570  o1rlimmul  15572  lo1add  15580  lo1mul  15581  climsqz  15594  climsqz2  15595  rlimsqzlem  15602  lo1le  15605  climbdd  15625  caucvgrlem  15626  caucvgrlem2  15628  caurcvg2  15631  iseralt  15638  cvgcmp  15770  cvgcmpce  15772  gcdcllem1  16459  absproddvds  16577  coprmprod  16621  coprmproddvdslem  16622  pcfac  16861  pockthg  16868  infpnlem1  16872  prmreclem2  16879  prmreclem3  16880  vdwlem11  16953  vdwlem13  16955  vdwnnlem3  16959  isacs2  17610  acsfn1  17618  acsfn2  17620  catpropd  17666  drsdirfi  18262  ipodrsima  18498  isacs5  18505  mrelatglb  18517  mrelatlub  18519  isgrpinv  18960  dfgrp3e  19007  issubg4  19112  gsmsymgreqlem2  19397  finodsubmsubg  19533  gexdvds  19550  gexcl3  19553  sylow2blem3  19588  cyggeninv  19849  gsummptnn0fz  19952  dprdff  19980  issubdrg  20752  acsfn1p  20771  cygznlem3  21544  psdmul  22154  mptcoe1fsupp  22200  cply1coe0bi  22288  gsummoncoe1  22294  evls1fpws  22355  scmatdmat  22498  mdetdiagid  22583  mdetunilem9  22603  cpmatmcllem  22701  m2cpminvid2lem  22737  decpmatmulsumfsupp  22756  pmatcollpw1lem1  22757  pmatcollpw2lem  22760  pmatcollpwfi  22765  pm2mpf1  22782  mptcoe1matfsupp  22785  mp2pm2mplem4  22792  pm2mpmhmlem1  22801  pm2mp  22808  chpdmat  22824  chpscmat  22825  cpmidpmatlem3  22855  cayhamlem4  22871  neiptopnei  23115  cncnp  23263  isnrm2  23341  isreg2  23360  2ndcdisj  23439  islly2  23467  dislly  23480  kgen2ss  23538  ptbasfi  23564  ptclsg  23598  prdstopn  23611  txtube  23623  txlm  23631  isr0  23720  filuni  23868  alexsubALTlem3  24032  ptcmplem3  24037  ptcmplem4  24038  tsmsxplem1  24136  prdsmet  24353  metequiv2  24493  metcnpi3  24529  nmoleub  24714  rescncf  24882  cncfco  24892  evth  24944  lebnumlem3  24948  xlebnum  24950  nmoleub2lem2  25101  nmhmcn  25105  lmmcvg  25246  cmetcaulem  25273  caubl  25293  bcth3  25316  ovollb2lem  25473  ovoliunlem2  25488  ovolicc2lem3  25504  ovolicc2lem4  25505  nulmbl2  25521  volsup  25541  ioombl1lem4  25546  dyadmax  25583  vitalilem2  25594  vitalilem5  25597  mbfi1flimlem  25707  itg2seq  25727  itg2addlem  25743  itgcn  25830  limciun  25879  rolle  25975  dvfsumrlim  26016  itgsubst  26034  aannenlem1  26312  aalioulem3  26318  ulmcaulem  26377  ulmcau  26378  ulmss  26380  ulmbdd  26381  ulmcn  26382  ulmdvlem3  26385  mtest  26387  iblulm  26390  itgulm  26391  rlimcnp  26947  xrlimcnp  26950  rlimcxp  26955  o1cxp  26956  amgm  26972  lgambdd  27018  ftalem2  27055  isppw2  27096  mumullem2  27161  2sqlem6  27404  chtppilimlem2  27455  chtppilim  27456  pntrsumbnd2  27548  pntlem3  27590  nosupbnd1lem5  27694  noinfbnd1lem5  27709  noetasuplem4  27718  noetainflem4  27722  negbdaylem  28066  mulsuniflem  28159  elreno2  28505  isperp2  28801  axeuclidlem  29049  axeuclid  29050  uhgrnbgr0nb  29441  vtxdginducedm1fi  29631  cusgrrusgr  29668  rusgrpropnb  29670  rusgrpropedg  29671  rusgrpropadjvtx  29672  upgrewlkle2  29693  wlkvtxiedg  29711  upgrwlkvtxedg  29731  uspgr2wlkeq  29732  redwlk  29757  wlkdlem2  29768  lfgrwlkprop  29772  2pthnloop  29817  upgr2pthnlp  29818  pthdlem1  29852  pthdlem2lem  29853  wlkiswwlks1  29953  wlkiswwlks2lem4  29958  wwlksm1edg  29967  wwlksnred  29978  clwwlkccatlem  30077  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  cusconngr  30279  eucrctshift  30331  2pthfrgr  30372  3cyclfrgr  30376  nmoub3i  30862  ubthlem1  30959  ubthlem3  30961  ocsh  31372  chintcli  31420  chscllem2  31727  nmopub2tALT  31998  nmfnleub2  32015  lnconi  32122  riesz1  32154  rnbra  32196  leopadd  32221  leopmuli  32222  leoptr  32226  dmdbr3  32394  dmdbr4  32395  dmdbr5  32397  mdsl0  32399  mdsymlem6  32497  cdj1i  32522  acunirnmpt  32751  xrge0infss  32852  isdrng4  33379  elrspunidl  33511  cmppcmp  34042  zarclsiin  34055  lmxrge0  34136  ftc2re  34782  cvmlift2lem12  35542  opnrebl2  36549  neibastop1  36587  neibastop2lem  36588  neibastop3  36590  finixpnum  37972  lindsenlbs  37982  matunitlindflem1  37983  matunitlindflem2  37984  ptrecube  37987  poimirlem26  38013  poimirlem27  38014  poimirlem29  38016  poimirlem30  38017  poimir  38020  heicant  38022  itg2addnclem  38038  itg2addnclem3  38040  itg2addnc  38041  filbcmb  38107  nninfnub  38118  geomcau  38126  sstotbnd2  38141  isbndx  38149  prdsbnd  38160  heibor1lem  38176  heiborlem1  38178  heibor  38188  rrncmslem  38199  intidl  38396  pclclN  40383  lauteq  40587  ltrnid  40627  mapdh9a  42281  primrootscoprmpow  42584  sticksstones3  42633  aks5lem5a  42676  aks5lem6  42677  fltaccoprm  43090  fltabcoprm  43092  flt4lem5  43100  elrfirn2  43145  isnacs3  43159  rencldnfilem  43265  kelac1  43508  naddgeoa  43839  neik0pk1imk0  44491  cvgdvgrat  44757  neglimc  46090  limsupub  46147  limsuppnflem  46153  limsupre3lem  46175  limsupvaluz2  46181  supcnvlimsup  46183  climuzlem  46186  liminfval2  46211  limsupgtlem  46220  liminflelimsupuz  46228  liminflimsupclim  46250  xlimpnfxnegmnf  46257  liminflimsupxrre  46260  xlimmnfv  46277  xlimpnfv  46281  stoweidlem7  46450  fourierdlem73  46622  sge0isum  46870  meaiuninc3v  46927  preimageiingt  47163  preimaleiinlt  47164  smflimlem3  47216  smflimlem4  47217  cfsetsnfsetfo  47523  2reu8i  47576  iccpartres  47893  uhgrimisgrgric  48422  grlictr  48506  clnbgr3stgrgrlim  48510  clnbgr3stgrgrlic  48511  upwlkwlk  48630  upgrwlkupwlk  48631  copisnmnd  48660  2zrngnmlid2  48748  ply1mulgsumlem1  48877  ply1mulgsumlem3  48879  ply1mulgsumlem4  48880  snlindsntor  48962  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  iinfsubc  49548