Theorem ralimdva 3174

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  ralimdv  3176  ralimdvva  3209  wereu2  5652  frpomin  6338  fveqressseq  7073  f1mpt  7259  isores3  7337  caofrss  7718  caoftrn  7720  sorpssuni  7734  sorpssint  7735  onint  7790  xpord3inddlem  8153  smogt  8357  fisupg  9259  ixpfi2  9318  fissuni  9325  indexfi  9328  fiinfg  9472  wemaplem2  9520  rankonidlem  9811  ac5num  10040  acni2  10050  acndom2  10058  alephle  10092  dfac5  10132  cfsmolem  10273  isf34lem7  10382  isf34lem6  10383  fin1a2s  10417  acncc  10443  ttukeylem6  10517  fpwwe2lem7  10647  gchina  10709  inar1  10785  tskord  10790  grudomon  10827  grur1a  10829  dedekind  11398  fimaxre  12184  fiminre  12187  uzwo  12961  xrsupsslem  13360  xrinfmsslem  13361  fsuppmapnn0fiub0  14058  rexanre  15435  rexuz3  15437  rexico  15442  cau3lem  15443  limsupval2  15568  rlim2lt  15585  rlim3  15586  lo1bdd2  15612  lo1bddrp  15613  o1lo1  15625  climrlim2  15635  2clim  15660  o1co  15674  rlimcn1  15676  rlimcn3  15678  climcn1  15680  climcn2  15681  subcn2  15683  o1of2  15701  rlimo1  15705  o1rlimmul  15707  lo1add  15715  lo1mul  15716  climsqz  15729  climsqz2  15730  rlimsqzlem  15737  lo1le  15740  climbdd  15760  caucvgrlem  15761  caucvgrlem2  15763  caurcvg2  15766  iseralt  15773  cvgcmp  15904  cvgcmpce  15906  gcdcllem1  16590  absproddvds  16708  coprmprod  16752  coprmproddvdslem  16753  pcfac  16992  pockthg  16999  infpnlem1  17003  prmreclem2  17010  prmreclem3  17011  vdwlem11  17084  vdwlem13  17086  vdwnnlem3  17090  isacs2  17742  acsfn1  17750  acsfn2  17752  catpropd  17798  drsdirfi  18394  ipodrsima  18630  isacs5  18637  mrelatglb  18649  mrelatlub  18651  isgrpinv  19118  dfgrp3e  19164  issubg4  19270  gsmsymgreqlem2  19559  finodsubmsubg  19695  gexdvds  19712  gexcl3  19715  sylow2blem3  19750  cyggeninv  20011  gsummptnn0fz  20114  dprdff  20142  isdrng4  20903  issubdrg  20947  acsfn1p  20966  cygznlem3  21783  lindsenlbs  22065  psdmul  22395  mptcoe1fsupp  22441  cply1coe0bi  22528  gsummoncoe1  22534  evls1fpws  22595  scmatdmat  22738  mdetdiagid  22823  mdetunilem9  22843  matunitlindflem1  22902  matunitlindflem2  22903  cpmatmcllem  22944  m2cpminvid2lem  22980  decpmatmulsumfsupp  22999  pmatcollpw1lem1  23000  pmatcollpw2lem  23003  pmatcollpwfi  23008  pm2mpf1  23025  mptcoe1matfsupp  23028  mp2pm2mplem4  23035  pm2mpmhmlem1  23044  pm2mp  23051  chpdmat  23067  chpscmat  23068  cpmidpmatlem3  23098  cayhamlem4  23114  neiptopnei  23358  cncnp  23506  isnrm2  23584  isreg2  23603  2ndcdisj  23683  islly2  23711  dislly  23724  kgen2ss  23782  ptbasfi  23808  ptclsg  23842  prdstopn  23855  txtube  23867  txlm  23875  isr0  23964  filuni  24112  alexsubALTlem3  24276  ptcmplem3  24281  ptcmplem4  24282  tsmsxplem1  24380  prdsmet  24597  metequiv2  24737  metcnpi3  24773  nmoleub  24958  rescncf  25126  cncfco  25136  evth  25188  lebnumlem3  25192  xlebnum  25194  nmoleub2lem2  25345  nmhmcn  25349  lmmcvg  25490  cmetcaulem  25517  caubl  25537  bcth3  25560  ovollb2lem  25717  ovoliunlem2  25732  ovolicc2lem3  25748  ovolicc2lem4  25749  nulmbl2  25765  volsup  25785  ioombl1lem4  25790  dyadmax  25827  vitalilem2  25838  vitalilem5  25841  mbfi1flimlem  25951  itg2seq  25971  itg2addlem  25987  itgcn  26073  limciun  26122  rolle  26218  dvfsumrlim  26259  itgsubst  26277  aannenlem1  26565  aalioulem3  26571  ulmcaulem  26631  ulmcau  26632  ulmss  26634  ulmbdd  26635  ulmcn  26636  ulmdvlem3  26639  mtest  26641  iblulm  26644  itgulm  26645  rlimcnp  27203  xrlimcnp  27206  rlimcxp  27211  o1cxp  27212  amgm  27228  lgambdd  27274  ftalem2  27311  isppw2  27352  mumullem2  27417  2sqlem6  27660  chtppilimlem2  27711  chtppilim  27712  pntrsumbnd2  27804  pntlem3  27846  nosupbnd1lem5  27949  noinfbnd1lem5  27964  noetasuplem4  27973  noetainflem4  27977  negbdaylem  28322  mulsuniflem  28415  elreno2  28761  isperp2  29070  axeuclidlem  29420  axeuclid  29421  uhgrnbgr0nb  29815  vtxdginducedm1fi  30005  cusgrrusgr  30042  rusgrpropnb  30044  rusgrpropedg  30045  rusgrpropadjvtx  30046  upgrewlkle2  30067  wlkvtxiedg  30085  upgrwlkvtxedg  30105  uspgr2wlkeq  30106  redwlk  30131  wlkdlem2  30142  lfgrwlkprop  30150  2pthnloop  30197  upgr2pthnlp  30198  pthdlem1  30232  pthdlem2lem  30233  wlkiswwlks1  30336  wlkiswwlks2lem4  30341  wwlksm1edg  30350  wwlksnred  30361  clwwlkccatlem  30460  clwlkclwwlklem2a  30469  clwlkclwwlklem2  30471  cusconngr  30672  eucrctshift  30724  2pthfrgr  30765  3cyclfrgr  30769  nmoub3i  31255  ubthlem1  31352  ubthlem3  31354  ocsh  31765  chintcli  31813  chscllem2  32120  nmopub2tALT  32391  nmfnleub2  32408  lnconi  32515  riesz1  32547  rnbra  32589  leopadd  32614  leopmuli  32615  leoptr  32619  dmdbr3  32787  dmdbr4  32788  dmdbr5  32790  mdsl0  32792  mdsymlem6  32890  cdj1i  32915  acunirnmpt  33133  xrge0infss  33232  elrspunidl  33857  dflring2  33904  cmppcmp  34369  zarclsiin  34382  lmxrge0  34463  ftc2re  35107  cvmlift2lem12  35894  nmulrid  36778  opnrebl2  36941  neibastop1  36979  neibastop2lem  36980  neibastop3  36982  finixpnum  38360  ptrecube  38370  poimirlem26  38396  poimirlem27  38397  poimirlem29  38399  poimirlem30  38400  poimir  38403  heicant  38405  itg2addnclem  38421  itg2addnclem3  38423  itg2addnc  38424  filbcmb  38491  nninfnub  38502  geomcau  38510  sstotbnd2  38525  isbndx  38533  prdsbnd  38544  heibor1lem  38560  heiborlem1  38562  heibor  38572  rrncmslem  38583  intidl  38780  pclclN  40765  lauteq  40969  ltrnid  41009  mapdh9a  42663  primrootscoprmpow  42966  sticksstones3  43015  aks5lem5a  43058  aks5lem6  43059  fltaccoprm  43487  fltabcoprm  43489  flt4lem5  43497  elrfirn2  43542  isnacs3  43556  rencldnfilem  43662  kelac1  43905  naddgeoa  44236  neik0pk1imk0  44888  cvgdvgrat  45138  neglimc  46476  limsupub  46533  limsuppnflem  46539  limsupre3lem  46561  limsupvaluz2  46567  supcnvlimsup  46569  climuzlem  46572  liminfval2  46597  limsupgtlem  46606  liminflelimsupuz  46614  liminflimsupclim  46636  xlimpnfxnegmnf  46643  liminflimsupxrre  46646  xlimmnfv  46663  xlimpnfv  46667  stoweidlem7  46836  fourierdlem73  47008  sge0isum  47256  meaiuninc3v  47313  preimageiingt  47549  preimaleiinlt  47550  smflimlem3  47602  smflimlem4  47603  cfsetsnfsetfo  47949  2reu8i  48002  iccpartres  48319  uhgrimisgrgric  48848  grlictr  48932  clnbgr3stgrgrlim  48936  clnbgr3stgrgrlic  48937  upwlkwlk  49056  upgrwlkupwlk  49057  copisnmnd  49085  2zrngnmlid2  49173  ply1mulgsumlem1  49317  ply1mulgsumlem3  49319  ply1mulgsumlem4  49320  snlindsntor  49402  eenglngeehlnmlem1  49668  eenglngeehlnmlem2  49669  iinfsubc  49985