Theorem ralimdva 3090

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3056

This theorem is referenced by:  ralimdv  3091  ralimdvva  3092  wereu2  5533  frpomin  6172  fveqressseq  6878  f1mpt  7051  isores3  7122  caofrss  7482  caoftrn  7484  sorpssuni  7498  sorpssint  7499  onint  7552  smogt  8082  fisupg  8897  ixpfi2  8952  fissuni  8959  indexfi  8962  fiinfg  9093  wemaplem2  9141  rankonidlem  9409  ac5num  9615  acni2  9625  acndom2  9633  alephle  9667  dfac5  9707  cfsmolem  9849  isf34lem7  9958  isf34lem6  9959  fin1a2s  9993  acncc  10019  ttukeylem6  10093  fpwwe2lem7  10216  gchina  10278  inar1  10354  tskord  10359  grudomon  10396  grur1a  10398  dedekind  10960  fimaxre  11741  fiminre  11744  uzwo  12472  xrsupsslem  12862  xrinfmsslem  12863  fsuppmapnn0fiub0  13531  rexanre  14875  rexuz3  14877  rexico  14882  cau3lem  14883  limsupval2  15006  rlim2lt  15023  rlim3  15024  lo1bdd2  15050  lo1bddrp  15051  o1lo1  15063  climrlim2  15073  2clim  15098  o1co  15112  rlimcn1  15114  rlimcn3  15116  climcn1  15118  climcn2  15119  subcn2  15121  o1of2  15139  rlimo1  15143  o1rlimmul  15145  lo1add  15153  lo1mul  15154  climsqz  15167  climsqz2  15168  rlimsqzlem  15177  lo1le  15180  climbdd  15200  caucvgrlem  15201  caucvgrlem2  15203  caurcvg2  15206  iseralt  15213  cvgcmp  15343  cvgcmpce  15345  gcdcllem1  16021  absproddvds  16137  coprmprod  16181  coprmproddvdslem  16182  pcfac  16415  pockthg  16422  infpnlem1  16426  prmreclem2  16433  prmreclem3  16434  vdwlem11  16507  vdwlem13  16509  vdwnnlem3  16513  isacs2  17110  acsfn1  17118  acsfn2  17120  catpropd  17166  drsdirfi  17766  ipodrsima  18001  isacs5  18008  mrelatglb  18020  mrelatlub  18022  isgrpinv  18374  dfgrp3e  18417  issubg4  18516  gsmsymgreqlem2  18777  gexdvds  18927  gexcl3  18930  sylow2blem3  18965  cyggeninv  19221  gsummptnn0fz  19325  dprdff  19353  issubdrg  19779  acsfn1p  19797  cygznlem3  20488  mptcoe1fsupp  21090  cply1coe0bi  21175  gsummoncoe1  21179  scmatdmat  21366  mdetdiagid  21451  mdetunilem9  21471  cpmatmcllem  21569  m2cpminvid2lem  21605  decpmatmulsumfsupp  21624  pmatcollpw1lem1  21625  pmatcollpw2lem  21628  pmatcollpwfi  21633  pm2mpf1  21650  mptcoe1matfsupp  21653  mp2pm2mplem4  21660  pm2mpmhmlem1  21669  pm2mp  21676  chpdmat  21692  chpscmat  21693  cpmidpmatlem3  21723  cayhamlem4  21739  neiptopnei  21983  cncnp  22131  isnrm2  22209  isreg2  22228  2ndcdisj  22307  islly2  22335  dislly  22348  kgen2ss  22406  ptbasfi  22432  ptclsg  22466  prdstopn  22479  txtube  22491  txlm  22499  isr0  22588  filuni  22736  alexsubALTlem3  22900  ptcmplem3  22905  ptcmplem4  22906  tsmsxplem1  23004  prdsmet  23222  metequiv2  23362  metcnpi3  23398  nmoleub  23583  rescncf  23748  cncfco  23758  evth  23810  lebnumlem3  23814  xlebnum  23816  nmoleub2lem2  23967  nmhmcn  23971  lmmcvg  24112  cmetcaulem  24139  caubl  24159  bcth3  24182  ovollb2lem  24339  ovoliunlem2  24354  ovolicc2lem3  24370  ovolicc2lem4  24371  nulmbl2  24387  volsup  24407  ioombl1lem4  24412  dyadmax  24449  vitalilem2  24460  vitalilem5  24463  mbfi1flimlem  24574  itg2seq  24594  itg2addlem  24610  itgcn  24696  limciun  24745  rolle  24841  dvfsumrlim  24882  itgsubst  24900  aannenlem1  25175  aalioulem3  25181  ulmcaulem  25240  ulmcau  25241  ulmss  25243  ulmbdd  25244  ulmcn  25245  ulmdvlem3  25248  mtest  25250  iblulm  25253  itgulm  25254  rlimcnp  25802  xrlimcnp  25805  rlimcxp  25810  o1cxp  25811  amgm  25827  lgambdd  25873  ftalem2  25910  isppw2  25951  mumullem2  26016  2sqlem6  26258  chtppilimlem2  26309  chtppilim  26310  pntrsumbnd2  26402  pntlem3  26444  isperp2  26760  axeuclidlem  27007  axeuclid  27008  uhgrnbgr0nb  27396  vtxdginducedm1fi  27586  cusgrrusgr  27623  rusgrpropnb  27625  rusgrpropedg  27626  rusgrpropadjvtx  27627  upgrewlkle2  27648  wlkvtxiedg  27666  upgrwlkvtxedg  27686  uspgr2wlkeq  27687  redwlk  27714  wlkdlem2  27725  lfgrwlkprop  27729  2pthnloop  27772  upgr2pthnlp  27773  pthdlem1  27807  pthdlem2lem  27808  wlkiswwlks1  27905  wlkiswwlks2lem4  27910  wwlksm1edg  27919  wwlksnred  27930  clwwlkccatlem  28026  clwlkclwwlklem2a  28035  clwlkclwwlklem2  28037  cusconngr  28228  eucrctshift  28280  2pthfrgr  28321  3cyclfrgr  28325  nmoub3i  28808  ubthlem1  28905  ubthlem3  28907  ocsh  29318  chintcli  29366  chscllem2  29673  nmopub2tALT  29944  nmfnleub2  29961  lnconi  30068  riesz1  30100  rnbra  30142  leopadd  30167  leopmuli  30168  leoptr  30172  dmdbr3  30340  dmdbr4  30341  dmdbr5  30343  mdsl0  30345  mdsymlem6  30443  cdj1i  30468  acunirnmpt  30670  xrge0infss  30757  elrspunidl  31274  cmppcmp  31476  zarclsiin  31489  lmxrge0  31570  ftc2re  32244  cvmlift2lem12  32943  nosupbnd1lem5  33601  noinfbnd1lem5  33616  noetasuplem4  33625  noetainflem4  33629  opnrebl2  34196  neibastop1  34234  neibastop2lem  34235  neibastop3  34237  finixpnum  35448  lindsenlbs  35458  matunitlindflem1  35459  matunitlindflem2  35460  ptrecube  35463  poimirlem26  35489  poimirlem27  35490  poimirlem29  35492  poimirlem30  35493  poimir  35496  heicant  35498  itg2addnclem  35514  itg2addnclem3  35516  itg2addnc  35517  filbcmb  35584  nninfnub  35595  geomcau  35603  sstotbnd2  35618  isbndx  35626  prdsbnd  35637  heibor1lem  35653  heiborlem1  35655  heibor  35665  rrncmslem  35676  intidl  35873  pclclN  37591  lauteq  37795  ltrnid  37835  mapdh9a  39489  sticksstones3  39773  fltaccoprm  40121  fltabcoprm  40123  flt4lem5  40131  elrfirn2  40162  isnacs3  40176  rencldnfilem  40286  kelac1  40532  neik0pk1imk0  41275  cvgdvgrat  41545  neglimc  42806  limsupub  42863  limsuppnflem  42869  limsupre3lem  42891  limsupvaluz2  42897  supcnvlimsup  42899  climuzlem  42902  liminfval2  42927  limsupgtlem  42936  liminflelimsupuz  42944  liminflimsupclim  42966  xlimpnfxnegmnf  42973  liminflimsupxrre  42976  xlimmnfv  42993  xlimpnfv  42997  stoweidlem7  43166  fourierdlem73  43338  sge0isum  43583  meaiuninc3v  43640  preimageiingt  43872  preimaleiinlt  43873  smflimlem3  43923  smflimlem4  43924  cfsetsnfsetfo  44169  2reu8i  44220  iccpartres  44486  upwlkwlk  44917  upgrwlkupwlk  44918  copisnmnd  44979  2zrngnmlid2  45125  ply1mulgsumlem1  45343  ply1mulgsumlem3  45345  ply1mulgsumlem4  45346  snlindsntor  45428  eenglngeehlnmlem1  45699  eenglngeehlnmlem2  45700