Theorem ralimdva 3165

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3060

This theorem is referenced by:  ralimdv  3167  ralimdvva  3202  wereu2  5672  frpomin  6340  fveqressseq  7080  f1mpt  7262  isores3  7334  caofrss  7708  caoftrn  7710  sorpssuni  7724  sorpssint  7725  onint  7780  xpord3inddlem  8142  smogt  8369  fisupg  9293  ixpfi2  9352  fissuni  9359  indexfi  9362  fiinfg  9496  wemaplem2  9544  rankonidlem  9825  ac5num  10033  acni2  10043  acndom2  10051  alephle  10085  dfac5  10125  cfsmolem  10267  isf34lem7  10376  isf34lem6  10377  fin1a2s  10411  acncc  10437  ttukeylem6  10511  fpwwe2lem7  10634  gchina  10696  inar1  10772  tskord  10777  grudomon  10814  grur1a  10816  dedekind  11381  fimaxre  12162  fiminre  12165  uzwo  12899  xrsupsslem  13290  xrinfmsslem  13291  fsuppmapnn0fiub0  13962  rexanre  15297  rexuz3  15299  rexico  15304  cau3lem  15305  limsupval2  15428  rlim2lt  15445  rlim3  15446  lo1bdd2  15472  lo1bddrp  15473  o1lo1  15485  climrlim2  15495  2clim  15520  o1co  15534  rlimcn1  15536  rlimcn3  15538  climcn1  15540  climcn2  15541  subcn2  15543  o1of2  15561  rlimo1  15565  o1rlimmul  15567  lo1add  15575  lo1mul  15576  climsqz  15589  climsqz2  15590  rlimsqzlem  15599  lo1le  15602  climbdd  15622  caucvgrlem  15623  caucvgrlem2  15625  caurcvg2  15628  iseralt  15635  cvgcmp  15766  cvgcmpce  15768  gcdcllem1  16444  absproddvds  16558  coprmprod  16602  coprmproddvdslem  16603  pcfac  16836  pockthg  16843  infpnlem1  16847  prmreclem2  16854  prmreclem3  16855  vdwlem11  16928  vdwlem13  16930  vdwnnlem3  16934  isacs2  17601  acsfn1  17609  acsfn2  17611  catpropd  17657  drsdirfi  18262  ipodrsima  18498  isacs5  18505  mrelatglb  18517  mrelatlub  18519  isgrpinv  18914  dfgrp3e  18959  issubg4  19061  gsmsymgreqlem2  19340  finodsubmsubg  19476  gexdvds  19493  gexcl3  19496  sylow2blem3  19531  cyggeninv  19792  gsummptnn0fz  19895  dprdff  19923  issubdrg  20544  acsfn1p  20558  cygznlem3  21344  mptcoe1fsupp  21958  cply1coe0bi  22044  gsummoncoe1  22048  scmatdmat  22237  mdetdiagid  22322  mdetunilem9  22342  cpmatmcllem  22440  m2cpminvid2lem  22476  decpmatmulsumfsupp  22495  pmatcollpw1lem1  22496  pmatcollpw2lem  22499  pmatcollpwfi  22504  pm2mpf1  22521  mptcoe1matfsupp  22524  mp2pm2mplem4  22531  pm2mpmhmlem1  22540  pm2mp  22547  chpdmat  22563  chpscmat  22564  cpmidpmatlem3  22594  cayhamlem4  22610  neiptopnei  22856  cncnp  23004  isnrm2  23082  isreg2  23101  2ndcdisj  23180  islly2  23208  dislly  23221  kgen2ss  23279  ptbasfi  23305  ptclsg  23339  prdstopn  23352  txtube  23364  txlm  23372  isr0  23461  filuni  23609  alexsubALTlem3  23773  ptcmplem3  23778  ptcmplem4  23779  tsmsxplem1  23877  prdsmet  24096  metequiv2  24239  metcnpi3  24275  nmoleub  24468  rescncf  24637  cncfco  24647  evth  24705  lebnumlem3  24709  xlebnum  24711  nmoleub2lem2  24863  nmhmcn  24867  lmmcvg  25009  cmetcaulem  25036  caubl  25056  bcth3  25079  ovollb2lem  25237  ovoliunlem2  25252  ovolicc2lem3  25268  ovolicc2lem4  25269  nulmbl2  25285  volsup  25305  ioombl1lem4  25310  dyadmax  25347  vitalilem2  25358  vitalilem5  25361  mbfi1flimlem  25472  itg2seq  25492  itg2addlem  25508  itgcn  25594  limciun  25643  rolle  25742  dvfsumrlim  25783  itgsubst  25801  aannenlem1  26077  aalioulem3  26083  ulmcaulem  26142  ulmcau  26143  ulmss  26145  ulmbdd  26146  ulmcn  26147  ulmdvlem3  26150  mtest  26152  iblulm  26155  itgulm  26156  rlimcnp  26706  xrlimcnp  26709  rlimcxp  26714  o1cxp  26715  amgm  26731  lgambdd  26777  ftalem2  26814  isppw2  26855  mumullem2  26920  2sqlem6  27162  chtppilimlem2  27213  chtppilim  27214  pntrsumbnd2  27306  pntlem3  27348  nosupbnd1lem5  27451  noinfbnd1lem5  27466  noetasuplem4  27475  noetainflem4  27479  negsbdaylem  27769  mulsuniflem  27843  isperp2  28233  axeuclidlem  28487  axeuclid  28488  uhgrnbgr0nb  28878  vtxdginducedm1fi  29068  cusgrrusgr  29105  rusgrpropnb  29107  rusgrpropedg  29108  rusgrpropadjvtx  29109  upgrewlkle2  29130  wlkvtxiedg  29149  upgrwlkvtxedg  29169  uspgr2wlkeq  29170  redwlk  29196  wlkdlem2  29207  lfgrwlkprop  29211  2pthnloop  29255  upgr2pthnlp  29256  pthdlem1  29290  pthdlem2lem  29291  wlkiswwlks1  29388  wlkiswwlks2lem4  29393  wwlksm1edg  29402  wwlksnred  29413  clwwlkccatlem  29509  clwlkclwwlklem2a  29518  clwlkclwwlklem2  29520  cusconngr  29711  eucrctshift  29763  2pthfrgr  29804  3cyclfrgr  29808  nmoub3i  30293  ubthlem1  30390  ubthlem3  30392  ocsh  30803  chintcli  30851  chscllem2  31158  nmopub2tALT  31429  nmfnleub2  31446  lnconi  31553  riesz1  31585  rnbra  31627  leopadd  31652  leopmuli  31653  leoptr  31657  dmdbr3  31825  dmdbr4  31826  dmdbr5  31828  mdsl0  31830  mdsymlem6  31928  cdj1i  31953  acunirnmpt  32151  xrge0infss  32240  isdrng4  32665  elrspunidl  32820  evls1fpws  32920  cmppcmp  33136  zarclsiin  33149  lmxrge0  33230  ftc2re  33908  cvmlift2lem12  34603  opnrebl2  35509  neibastop1  35547  neibastop2lem  35548  neibastop3  35550  finixpnum  36776  lindsenlbs  36786  matunitlindflem1  36787  matunitlindflem2  36788  ptrecube  36791  poimirlem26  36817  poimirlem27  36818  poimirlem29  36820  poimirlem30  36821  poimir  36824  heicant  36826  itg2addnclem  36842  itg2addnclem3  36844  itg2addnc  36845  filbcmb  36911  nninfnub  36922  geomcau  36930  sstotbnd2  36945  isbndx  36953  prdsbnd  36964  heibor1lem  36980  heiborlem1  36982  heibor  36992  rrncmslem  37003  intidl  37200  pclclN  39065  lauteq  39269  ltrnid  39309  mapdh9a  40963  sticksstones3  41270  fltaccoprm  41684  fltabcoprm  41686  flt4lem5  41694  elrfirn2  41736  isnacs3  41750  rencldnfilem  41860  kelac1  42107  naddgeoa  42447  neik0pk1imk0  43100  cvgdvgrat  43374  neglimc  44661  limsupub  44718  limsuppnflem  44724  limsupre3lem  44746  limsupvaluz2  44752  supcnvlimsup  44754  climuzlem  44757  liminfval2  44782  limsupgtlem  44791  liminflelimsupuz  44799  liminflimsupclim  44821  xlimpnfxnegmnf  44828  liminflimsupxrre  44831  xlimmnfv  44848  xlimpnfv  44852  stoweidlem7  45021  fourierdlem73  45193  sge0isum  45441  meaiuninc3v  45498  preimageiingt  45734  preimaleiinlt  45735  smflimlem3  45787  smflimlem4  45788  cfsetsnfsetfo  46068  2reu8i  46119  iccpartres  46384  upwlkwlk  46815  upgrwlkupwlk  46816  copisnmnd  46845  2zrngnmlid2  46937  ply1mulgsumlem1  47154  ply1mulgsumlem3  47156  ply1mulgsumlem4  47157  snlindsntor  47239  eenglngeehlnmlem1  47510  eenglngeehlnmlem2  47511