Theorem ralimdva 3183

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3086

This theorem is referenced by:  ralimdv  3185  ralimdvva  3218  wereu2  5659  frpomin  6342  fveqressseq  7075  f1mpt  7260  isores3  7334  caofrss  7714  caoftrn  7716  sorpssuni  7730  sorpssint  7731  onint  7789  xpord3inddlem  8150  smogt  8354  fisupg  9248  ixpfi2  9307  fissuni  9314  indexfi  9317  fiinfg  9461  wemaplem2  9509  rankonidlem  9800  ac5num  10020  acni2  10030  acndom2  10038  alephle  10072  dfac5  10112  cfsmolem  10254  isf34lem7  10363  isf34lem6  10364  fin1a2s  10398  acncc  10424  ttukeylem6  10498  fpwwe2lem7  10622  gchina  10684  inar1  10760  tskord  10765  grudomon  10802  grur1a  10804  dedekind  11373  fimaxre  12159  fiminre  12162  uzwo  12935  xrsupsslem  13333  xrinfmsslem  13334  fsuppmapnn0fiub0  14029  rexanre  15398  rexuz3  15400  rexico  15405  cau3lem  15406  limsupval2  15531  rlim2lt  15548  rlim3  15549  lo1bdd2  15575  lo1bddrp  15576  o1lo1  15588  climrlim2  15598  2clim  15623  o1co  15637  rlimcn1  15639  rlimcn3  15641  climcn1  15643  climcn2  15644  subcn2  15646  o1of2  15664  rlimo1  15668  o1rlimmul  15670  lo1add  15678  lo1mul  15679  climsqz  15692  climsqz2  15693  rlimsqzlem  15700  lo1le  15703  climbdd  15723  caucvgrlem  15724  caucvgrlem2  15726  caurcvg2  15729  iseralt  15736  cvgcmp  15868  cvgcmpce  15870  gcdcllem1  16557  absproddvds  16675  coprmprod  16719  coprmproddvdslem  16720  pcfac  16959  pockthg  16966  infpnlem1  16970  prmreclem2  16977  prmreclem3  16978  vdwlem11  17051  vdwlem13  17053  vdwnnlem3  17057  isacs2  17709  acsfn1  17717  acsfn2  17719  catpropd  17765  drsdirfi  18361  ipodrsima  18597  isacs5  18604  mrelatglb  18616  mrelatlub  18618  isgrpinv  19060  dfgrp3e  19106  issubg4  19212  gsmsymgreqlem2  19501  finodsubmsubg  19637  gexdvds  19654  gexcl3  19657  sylow2blem3  19692  cyggeninv  19953  gsummptnn0fz  20056  dprdff  20084  issubdrg  20861  acsfn1p  20880  cygznlem3  21688  psdmul  22298  mptcoe1fsupp  22344  cply1coe0bi  22431  gsummoncoe1  22437  evls1fpws  22498  scmatdmat  22641  mdetdiagid  22726  mdetunilem9  22746  cpmatmcllem  22844  m2cpminvid2lem  22880  decpmatmulsumfsupp  22899  pmatcollpw1lem1  22900  pmatcollpw2lem  22903  pmatcollpwfi  22908  pm2mpf1  22925  mptcoe1matfsupp  22928  mp2pm2mplem4  22935  pm2mpmhmlem1  22944  pm2mp  22951  chpdmat  22967  chpscmat  22968  cpmidpmatlem3  22998  cayhamlem4  23014  neiptopnei  23258  cncnp  23406  isnrm2  23484  isreg2  23503  2ndcdisj  23582  islly2  23610  dislly  23623  kgen2ss  23681  ptbasfi  23707  ptclsg  23741  prdstopn  23754  txtube  23766  txlm  23774  isr0  23863  filuni  24011  alexsubALTlem3  24175  ptcmplem3  24180  ptcmplem4  24181  tsmsxplem1  24279  prdsmet  24496  metequiv2  24636  metcnpi3  24672  nmoleub  24857  rescncf  25025  cncfco  25035  evth  25087  lebnumlem3  25091  xlebnum  25093  nmoleub2lem2  25244  nmhmcn  25248  lmmcvg  25389  cmetcaulem  25416  caubl  25436  bcth3  25459  ovollb2lem  25616  ovoliunlem2  25631  ovolicc2lem3  25647  ovolicc2lem4  25648  nulmbl2  25664  volsup  25684  ioombl1lem4  25689  dyadmax  25726  vitalilem2  25737  vitalilem5  25740  mbfi1flimlem  25850  itg2seq  25870  itg2addlem  25886  itgcn  25973  limciun  26022  rolle  26118  dvfsumrlim  26159  itgsubst  26177  aannenlem1  26458  aalioulem3  26464  ulmcaulem  26523  ulmcau  26524  ulmss  26526  ulmbdd  26527  ulmcn  26528  ulmdvlem3  26531  mtest  26533  iblulm  26536  itgulm  26537  rlimcnp  27096  xrlimcnp  27099  rlimcxp  27104  o1cxp  27105  amgm  27121  lgambdd  27167  ftalem2  27204  isppw2  27245  mumullem2  27310  2sqlem6  27553  chtppilimlem2  27604  chtppilim  27605  pntrsumbnd2  27697  pntlem3  27739  nosupbnd1lem5  27842  noinfbnd1lem5  27857  noetasuplem4  27866  noetainflem4  27870  negbdaylem  28215  mulsuniflem  28308  elreno2  28654  isperp2  28954  axeuclidlem  29253  axeuclid  29254  uhgrnbgr0nb  29645  vtxdginducedm1fi  29835  cusgrrusgr  29872  rusgrpropnb  29874  rusgrpropedg  29875  rusgrpropadjvtx  29876  upgrewlkle2  29897  wlkvtxiedg  29915  upgrwlkvtxedg  29935  uspgr2wlkeq  29936  redwlk  29961  wlkdlem2  29972  lfgrwlkprop  29976  2pthnloop  30021  upgr2pthnlp  30022  pthdlem1  30056  pthdlem2lem  30057  wlkiswwlks1  30157  wlkiswwlks2lem4  30162  wwlksm1edg  30171  wwlksnred  30182  clwwlkccatlem  30281  clwlkclwwlklem2a  30290  clwlkclwwlklem2  30292  cusconngr  30483  eucrctshift  30535  2pthfrgr  30576  3cyclfrgr  30580  nmoub3i  31066  ubthlem1  31163  ubthlem3  31165  ocsh  31576  chintcli  31624  chscllem2  31931  nmopub2tALT  32202  nmfnleub2  32219  lnconi  32326  riesz1  32358  rnbra  32400  leopadd  32425  leopmuli  32426  leoptr  32430  dmdbr3  32598  dmdbr4  32599  dmdbr5  32601  mdsl0  32603  mdsymlem6  32701  cdj1i  32726  acunirnmpt  32945  xrge0infss  33046  isdrng4  33559  elrspunidl  33680  dflring2  33728  cmppcmp  34193  zarclsiin  34206  lmxrge0  34287  ftc2re  34930  cvmlift2lem12  35705  opnrebl2  36721  neibastop1  36759  neibastop2lem  36760  neibastop3  36762  finixpnum  38144  lindsenlbs  38154  matunitlindflem1  38155  matunitlindflem2  38156  ptrecube  38159  poimirlem26  38185  poimirlem27  38186  poimirlem29  38188  poimirlem30  38189  poimir  38192  heicant  38194  itg2addnclem  38210  itg2addnclem3  38212  itg2addnc  38213  filbcmb  38279  nninfnub  38290  geomcau  38298  sstotbnd2  38313  isbndx  38321  prdsbnd  38332  heibor1lem  38348  heiborlem1  38350  heibor  38360  rrncmslem  38371  intidl  38568  pclclN  40555  lauteq  40759  ltrnid  40799  mapdh9a  42453  primrootscoprmpow  42756  sticksstones3  42805  aks5lem5a  42848  aks5lem6  42849  fltaccoprm  43264  fltabcoprm  43266  flt4lem5  43274  elrfirn2  43319  isnacs3  43333  rencldnfilem  43439  kelac1  43682  naddgeoa  44013  neik0pk1imk0  44665  cvgdvgrat  44915  neglimc  46253  limsupub  46310  limsuppnflem  46316  limsupre3lem  46338  limsupvaluz2  46344  supcnvlimsup  46346  climuzlem  46349  liminfval2  46374  limsupgtlem  46383  liminflelimsupuz  46391  liminflimsupclim  46413  xlimpnfxnegmnf  46420  liminflimsupxrre  46423  xlimmnfv  46440  xlimpnfv  46444  stoweidlem7  46613  fourierdlem73  46785  sge0isum  47033  meaiuninc3v  47090  preimageiingt  47326  preimaleiinlt  47327  smflimlem3  47379  smflimlem4  47380  cfsetsnfsetfo  47686  2reu8i  47739  iccpartres  48056  uhgrimisgrgric  48585  grlictr  48669  clnbgr3stgrgrlim  48673  clnbgr3stgrgrlic  48674  upwlkwlk  48793  upgrwlkupwlk  48794  copisnmnd  48823  2zrngnmlid2  48911  ply1mulgsumlem1  49051  ply1mulgsumlem3  49053  ply1mulgsumlem4  49054  snlindsntor  49136  eenglngeehlnmlem1  49402  eenglngeehlnmlem2  49403  iinfsubc  49721