Theorem ralimdva 3173

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3068

This theorem is referenced by:  ralimdv  3175  ralimdvva  3212  wereu2  5697  frpomin  6372  fveqressseq  7113  f1mpt  7298  isores3  7371  caofrss  7751  caoftrn  7753  sorpssuni  7767  sorpssint  7768  onint  7826  xpord3inddlem  8195  smogt  8423  fisupg  9352  ixpfi2  9420  fissuni  9427  indexfi  9430  fiinfg  9568  wemaplem2  9616  rankonidlem  9897  ac5num  10105  acni2  10115  acndom2  10123  alephle  10157  dfac5  10198  cfsmolem  10339  isf34lem7  10448  isf34lem6  10449  fin1a2s  10483  acncc  10509  ttukeylem6  10583  fpwwe2lem7  10706  gchina  10768  inar1  10844  tskord  10849  grudomon  10886  grur1a  10888  dedekind  11453  fimaxre  12239  fiminre  12242  uzwo  12976  xrsupsslem  13369  xrinfmsslem  13370  fsuppmapnn0fiub0  14044  rexanre  15395  rexuz3  15397  rexico  15402  cau3lem  15403  limsupval2  15526  rlim2lt  15543  rlim3  15544  lo1bdd2  15570  lo1bddrp  15571  o1lo1  15583  climrlim2  15593  2clim  15618  o1co  15632  rlimcn1  15634  rlimcn3  15636  climcn1  15638  climcn2  15639  subcn2  15641  o1of2  15659  rlimo1  15663  o1rlimmul  15665  lo1add  15673  lo1mul  15674  climsqz  15687  climsqz2  15688  rlimsqzlem  15697  lo1le  15700  climbdd  15720  caucvgrlem  15721  caucvgrlem2  15723  caurcvg2  15726  iseralt  15733  cvgcmp  15864  cvgcmpce  15866  gcdcllem1  16545  absproddvds  16664  coprmprod  16708  coprmproddvdslem  16709  pcfac  16946  pockthg  16953  infpnlem1  16957  prmreclem2  16964  prmreclem3  16965  vdwlem11  17038  vdwlem13  17040  vdwnnlem3  17044  isacs2  17711  acsfn1  17719  acsfn2  17721  catpropd  17767  drsdirfi  18375  ipodrsima  18611  isacs5  18618  mrelatglb  18630  mrelatlub  18632  isgrpinv  19033  dfgrp3e  19080  issubg4  19185  gsmsymgreqlem2  19473  finodsubmsubg  19609  gexdvds  19626  gexcl3  19629  sylow2blem3  19664  cyggeninv  19925  gsummptnn0fz  20028  dprdff  20056  issubdrg  20803  acsfn1p  20822  cygznlem3  21611  psdmul  22193  mptcoe1fsupp  22238  cply1coe0bi  22327  gsummoncoe1  22333  evls1fpws  22394  scmatdmat  22542  mdetdiagid  22627  mdetunilem9  22647  cpmatmcllem  22745  m2cpminvid2lem  22781  decpmatmulsumfsupp  22800  pmatcollpw1lem1  22801  pmatcollpw2lem  22804  pmatcollpwfi  22809  pm2mpf1  22826  mptcoe1matfsupp  22829  mp2pm2mplem4  22836  pm2mpmhmlem1  22845  pm2mp  22852  chpdmat  22868  chpscmat  22869  cpmidpmatlem3  22899  cayhamlem4  22915  neiptopnei  23161  cncnp  23309  isnrm2  23387  isreg2  23406  2ndcdisj  23485  islly2  23513  dislly  23526  kgen2ss  23584  ptbasfi  23610  ptclsg  23644  prdstopn  23657  txtube  23669  txlm  23677  isr0  23766  filuni  23914  alexsubALTlem3  24078  ptcmplem3  24083  ptcmplem4  24084  tsmsxplem1  24182  prdsmet  24401  metequiv2  24544  metcnpi3  24580  nmoleub  24773  rescncf  24942  cncfco  24952  evth  25010  lebnumlem3  25014  xlebnum  25016  nmoleub2lem2  25168  nmhmcn  25172  lmmcvg  25314  cmetcaulem  25341  caubl  25361  bcth3  25384  ovollb2lem  25542  ovoliunlem2  25557  ovolicc2lem3  25573  ovolicc2lem4  25574  nulmbl2  25590  volsup  25610  ioombl1lem4  25615  dyadmax  25652  vitalilem2  25663  vitalilem5  25666  mbfi1flimlem  25777  itg2seq  25797  itg2addlem  25813  itgcn  25900  limciun  25949  rolle  26048  dvfsumrlim  26092  itgsubst  26110  aannenlem1  26388  aalioulem3  26394  ulmcaulem  26455  ulmcau  26456  ulmss  26458  ulmbdd  26459  ulmcn  26460  ulmdvlem3  26463  mtest  26465  iblulm  26468  itgulm  26469  rlimcnp  27026  xrlimcnp  27029  rlimcxp  27035  o1cxp  27036  amgm  27052  lgambdd  27098  ftalem2  27135  isppw2  27176  mumullem2  27241  2sqlem6  27485  chtppilimlem2  27536  chtppilim  27537  pntrsumbnd2  27629  pntlem3  27671  nosupbnd1lem5  27775  noinfbnd1lem5  27790  noetasuplem4  27799  noetainflem4  27803  negsbdaylem  28106  mulsuniflem  28193  isperp2  28741  axeuclidlem  28995  axeuclid  28996  uhgrnbgr0nb  29389  vtxdginducedm1fi  29580  cusgrrusgr  29617  rusgrpropnb  29619  rusgrpropedg  29620  rusgrpropadjvtx  29621  upgrewlkle2  29642  wlkvtxiedg  29661  upgrwlkvtxedg  29681  uspgr2wlkeq  29682  redwlk  29708  wlkdlem2  29719  lfgrwlkprop  29723  2pthnloop  29767  upgr2pthnlp  29768  pthdlem1  29802  pthdlem2lem  29803  wlkiswwlks1  29900  wlkiswwlks2lem4  29905  wwlksm1edg  29914  wwlksnred  29925  clwwlkccatlem  30021  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  cusconngr  30223  eucrctshift  30275  2pthfrgr  30316  3cyclfrgr  30320  nmoub3i  30805  ubthlem1  30902  ubthlem3  30904  ocsh  31315  chintcli  31363  chscllem2  31670  nmopub2tALT  31941  nmfnleub2  31958  lnconi  32065  riesz1  32097  rnbra  32139  leopadd  32164  leopmuli  32165  leoptr  32169  dmdbr3  32337  dmdbr4  32338  dmdbr5  32340  mdsl0  32342  mdsymlem6  32440  cdj1i  32465  acunirnmpt  32677  xrge0infss  32767  isdrng4  33264  elrspunidl  33421  cmppcmp  33804  zarclsiin  33817  lmxrge0  33898  ftc2re  34575  cvmlift2lem12  35282  opnrebl2  36287  neibastop1  36325  neibastop2lem  36326  neibastop3  36328  finixpnum  37565  lindsenlbs  37575  matunitlindflem1  37576  matunitlindflem2  37577  ptrecube  37580  poimirlem26  37606  poimirlem27  37607  poimirlem29  37609  poimirlem30  37610  poimir  37613  heicant  37615  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  filbcmb  37700  nninfnub  37711  geomcau  37719  sstotbnd2  37734  isbndx  37742  prdsbnd  37753  heibor1lem  37769  heiborlem1  37771  heibor  37781  rrncmslem  37792  intidl  37989  pclclN  39848  lauteq  40052  ltrnid  40092  mapdh9a  41746  primrootscoprmpow  42056  sticksstones3  42105  aks5lem5a  42148  aks5lem6  42149  fltaccoprm  42595  fltabcoprm  42597  flt4lem5  42605  elrfirn2  42652  isnacs3  42666  rencldnfilem  42776  kelac1  43020  naddgeoa  43356  neik0pk1imk0  44009  cvgdvgrat  44282  neglimc  45568  limsupub  45625  limsuppnflem  45631  limsupre3lem  45653  limsupvaluz2  45659  supcnvlimsup  45661  climuzlem  45664  liminfval2  45689  limsupgtlem  45698  liminflelimsupuz  45706  liminflimsupclim  45728  xlimpnfxnegmnf  45735  liminflimsupxrre  45738  xlimmnfv  45755  xlimpnfv  45759  stoweidlem7  45928  fourierdlem73  46100  sge0isum  46348  meaiuninc3v  46405  preimageiingt  46641  preimaleiinlt  46642  smflimlem3  46694  smflimlem4  46695  cfsetsnfsetfo  46975  2reu8i  47028  iccpartres  47292  uhgrimisgrgric  47783  grlictr  47832  upwlkwlk  47862  upgrwlkupwlk  47863  copisnmnd  47892  2zrngnmlid2  47980  ply1mulgsumlem1  48115  ply1mulgsumlem3  48117  ply1mulgsumlem4  48118  snlindsntor  48200  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472