Theorem ralimdva 3179

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

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

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 3082

This theorem is used by:  ralimdv  3181  ralimdvva  3214  wereu2  5660  frpomin  6345  fveqressseq  7078  f1mpt  7264  isores3  7342  caofrss  7723  caoftrn  7725  sorpssuni  7739  sorpssint  7740  onint  7795  xpord3inddlem  8156  smogt  8360  fisupg  9255  ixpfi2  9314  fissuni  9321  indexfi  9324  fiinfg  9468  wemaplem2  9516  rankonidlem  9807  ac5num  10036  acni2  10046  acndom2  10054  alephle  10088  dfac5  10128  cfsmolem  10269  isf34lem7  10378  isf34lem6  10379  fin1a2s  10413  acncc  10439  ttukeylem6  10513  fpwwe2lem7  10639  gchina  10701  inar1  10777  tskord  10782  grudomon  10819  grur1a  10821  dedekind  11390  fimaxre  12176  fiminre  12179  uzwo  12953  xrsupsslem  13351  xrinfmsslem  13352  fsuppmapnn0fiub0  14049  rexanre  15424  rexuz3  15426  rexico  15431  cau3lem  15432  limsupval2  15557  rlim2lt  15574  rlim3  15575  lo1bdd2  15601  lo1bddrp  15602  o1lo1  15614  climrlim2  15624  2clim  15649  o1co  15663  rlimcn1  15665  rlimcn3  15667  climcn1  15669  climcn2  15670  subcn2  15672  o1of2  15690  rlimo1  15694  o1rlimmul  15696  lo1add  15704  lo1mul  15705  climsqz  15718  climsqz2  15719  rlimsqzlem  15726  lo1le  15729  climbdd  15749  caucvgrlem  15750  caucvgrlem2  15752  caurcvg2  15755  iseralt  15762  cvgcmp  15893  cvgcmpce  15895  gcdcllem1  16581  absproddvds  16699  coprmprod  16743  coprmproddvdslem  16744  pcfac  16983  pockthg  16990  infpnlem1  16994  prmreclem2  17001  prmreclem3  17002  vdwlem11  17075  vdwlem13  17077  vdwnnlem3  17081  isacs2  17733  acsfn1  17741  acsfn2  17743  catpropd  17789  drsdirfi  18385  ipodrsima  18621  isacs5  18628  mrelatglb  18640  mrelatlub  18642  isgrpinv  19106  dfgrp3e  19152  issubg4  19258  gsmsymgreqlem2  19547  finodsubmsubg  19683  gexdvds  19700  gexcl3  19703  sylow2blem3  19738  cyggeninv  19999  gsummptnn0fz  20102  dprdff  20130  isdrng4  20891  issubdrg  20935  acsfn1p  20954  cygznlem3  21771  psdmul  22381  mptcoe1fsupp  22427  cply1coe0bi  22514  gsummoncoe1  22520  evls1fpws  22581  scmatdmat  22724  mdetdiagid  22809  mdetunilem9  22829  cpmatmcllem  22927  m2cpminvid2lem  22963  decpmatmulsumfsupp  22982  pmatcollpw1lem1  22983  pmatcollpw2lem  22986  pmatcollpwfi  22991  pm2mpf1  23008  mptcoe1matfsupp  23011  mp2pm2mplem4  23018  pm2mpmhmlem1  23027  pm2mp  23034  chpdmat  23050  chpscmat  23051  cpmidpmatlem3  23081  cayhamlem4  23097  neiptopnei  23341  cncnp  23489  isnrm2  23567  isreg2  23586  2ndcdisj  23666  islly2  23694  dislly  23707  kgen2ss  23765  ptbasfi  23791  ptclsg  23825  prdstopn  23838  txtube  23850  txlm  23858  isr0  23947  filuni  24095  alexsubALTlem3  24259  ptcmplem3  24264  ptcmplem4  24265  tsmsxplem1  24363  prdsmet  24580  metequiv2  24720  metcnpi3  24756  nmoleub  24941  rescncf  25109  cncfco  25119  evth  25171  lebnumlem3  25175  xlebnum  25177  nmoleub2lem2  25328  nmhmcn  25332  lmmcvg  25473  cmetcaulem  25500  caubl  25520  bcth3  25543  ovollb2lem  25700  ovoliunlem2  25715  ovolicc2lem3  25731  ovolicc2lem4  25732  nulmbl2  25748  volsup  25768  ioombl1lem4  25773  dyadmax  25810  vitalilem2  25821  vitalilem5  25824  mbfi1flimlem  25934  itg2seq  25954  itg2addlem  25970  itgcn  26057  limciun  26106  rolle  26202  dvfsumrlim  26243  itgsubst  26261  aannenlem1  26544  aalioulem3  26550  ulmcaulem  26610  ulmcau  26611  ulmss  26613  ulmbdd  26614  ulmcn  26615  ulmdvlem3  26618  mtest  26620  iblulm  26623  itgulm  26624  rlimcnp  27183  xrlimcnp  27186  rlimcxp  27191  o1cxp  27192  amgm  27208  lgambdd  27254  ftalem2  27291  isppw2  27332  mumullem2  27397  2sqlem6  27640  chtppilimlem2  27691  chtppilim  27692  pntrsumbnd2  27784  pntlem3  27826  nosupbnd1lem5  27929  noinfbnd1lem5  27944  noetasuplem4  27953  noetainflem4  27957  negbdaylem  28302  mulsuniflem  28395  elreno2  28741  isperp2  29048  axeuclidlem  29369  axeuclid  29370  uhgrnbgr0nb  29764  vtxdginducedm1fi  29954  cusgrrusgr  29991  rusgrpropnb  29993  rusgrpropedg  29994  rusgrpropadjvtx  29995  upgrewlkle2  30016  wlkvtxiedg  30034  upgrwlkvtxedg  30054  uspgr2wlkeq  30055  redwlk  30080  wlkdlem2  30091  lfgrwlkprop  30099  2pthnloop  30146  upgr2pthnlp  30147  pthdlem1  30181  pthdlem2lem  30182  wlkiswwlks1  30285  wlkiswwlks2lem4  30290  wwlksm1edg  30299  wwlksnred  30310  clwwlkccatlem  30409  clwlkclwwlklem2a  30418  clwlkclwwlklem2  30420  cusconngr  30615  eucrctshift  30667  2pthfrgr  30708  3cyclfrgr  30712  nmoub3i  31198  ubthlem1  31295  ubthlem3  31297  ocsh  31708  chintcli  31756  chscllem2  32063  nmopub2tALT  32334  nmfnleub2  32351  lnconi  32458  riesz1  32490  rnbra  32532  leopadd  32557  leopmuli  32558  leoptr  32562  dmdbr3  32730  dmdbr4  32731  dmdbr5  32733  mdsl0  32735  mdsymlem6  32833  cdj1i  32858  acunirnmpt  33077  xrge0infss  33177  elrspunidl  33802  dflring2  33849  cmppcmp  34314  zarclsiin  34327  lmxrge0  34408  ftc2re  35052  cvmlift2lem12  35845  nmulrid  36728  opnrebl2  36891  neibastop1  36929  neibastop2lem  36930  neibastop3  36932  finixpnum  38315  lindsenlbs  38325  matunitlindflem1  38326  matunitlindflem2  38327  ptrecube  38330  poimirlem26  38356  poimirlem27  38357  poimirlem29  38359  poimirlem30  38360  poimir  38363  heicant  38365  itg2addnclem  38381  itg2addnclem3  38383  itg2addnc  38384  filbcmb  38451  nninfnub  38462  geomcau  38470  sstotbnd2  38485  isbndx  38493  prdsbnd  38504  heibor1lem  38520  heiborlem1  38522  heibor  38532  rrncmslem  38543  intidl  38740  pclclN  40725  lauteq  40929  ltrnid  40969  mapdh9a  42623  primrootscoprmpow  42926  sticksstones3  42975  aks5lem5a  43018  aks5lem6  43019  fltaccoprm  43432  fltabcoprm  43434  flt4lem5  43442  elrfirn2  43487  isnacs3  43501  rencldnfilem  43607  kelac1  43850  naddgeoa  44181  neik0pk1imk0  44833  cvgdvgrat  45083  neglimc  46421  limsupub  46478  limsuppnflem  46484  limsupre3lem  46506  limsupvaluz2  46512  supcnvlimsup  46514  climuzlem  46517  liminfval2  46542  limsupgtlem  46551  liminflelimsupuz  46559  liminflimsupclim  46581  xlimpnfxnegmnf  46588  liminflimsupxrre  46591  xlimmnfv  46608  xlimpnfv  46612  stoweidlem7  46781  fourierdlem73  46953  sge0isum  47201  meaiuninc3v  47258  preimageiingt  47494  preimaleiinlt  47495  smflimlem3  47547  smflimlem4  47548  cfsetsnfsetfo  47857  2reu8i  47910  iccpartres  48227  uhgrimisgrgric  48756  grlictr  48840  clnbgr3stgrgrlim  48844  clnbgr3stgrgrlic  48845  upwlkwlk  48964  upgrwlkupwlk  48965  copisnmnd  48993  2zrngnmlid2  49081  ply1mulgsumlem1  49225  ply1mulgsumlem3  49227  ply1mulgsumlem4  49228  snlindsntor  49310  eenglngeehlnmlem1  49576  eenglngeehlnmlem2  49577  iinfsubc  49895