Theorem ralimdva 3108

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3069

This theorem is referenced by:  ralimdv  3109  ralimdvva  3126  wereu2  5586  frpomin  6243  fveqressseq  6957  f1mpt  7134  isores3  7206  caofrss  7569  caoftrn  7571  sorpssuni  7585  sorpssint  7586  onint  7640  smogt  8198  fisupg  9062  ixpfi2  9117  fissuni  9124  indexfi  9127  fiinfg  9258  wemaplem2  9306  rankonidlem  9586  ac5num  9792  acni2  9802  acndom2  9810  alephle  9844  dfac5  9884  cfsmolem  10026  isf34lem7  10135  isf34lem6  10136  fin1a2s  10170  acncc  10196  ttukeylem6  10270  fpwwe2lem7  10393  gchina  10455  inar1  10531  tskord  10536  grudomon  10573  grur1a  10575  dedekind  11138  fimaxre  11919  fiminre  11922  uzwo  12651  xrsupsslem  13041  xrinfmsslem  13042  fsuppmapnn0fiub0  13713  rexanre  15058  rexuz3  15060  rexico  15065  cau3lem  15066  limsupval2  15189  rlim2lt  15206  rlim3  15207  lo1bdd2  15233  lo1bddrp  15234  o1lo1  15246  climrlim2  15256  2clim  15281  o1co  15295  rlimcn1  15297  rlimcn3  15299  climcn1  15301  climcn2  15302  subcn2  15304  o1of2  15322  rlimo1  15326  o1rlimmul  15328  lo1add  15336  lo1mul  15337  climsqz  15350  climsqz2  15351  rlimsqzlem  15360  lo1le  15363  climbdd  15383  caucvgrlem  15384  caucvgrlem2  15386  caurcvg2  15389  iseralt  15396  cvgcmp  15528  cvgcmpce  15530  gcdcllem1  16206  absproddvds  16322  coprmprod  16366  coprmproddvdslem  16367  pcfac  16600  pockthg  16607  infpnlem1  16611  prmreclem2  16618  prmreclem3  16619  vdwlem11  16692  vdwlem13  16694  vdwnnlem3  16698  isacs2  17362  acsfn1  17370  acsfn2  17372  catpropd  17418  drsdirfi  18023  ipodrsima  18259  isacs5  18266  mrelatglb  18278  mrelatlub  18280  isgrpinv  18632  dfgrp3e  18675  issubg4  18774  gsmsymgreqlem2  19039  gexdvds  19189  gexcl3  19192  sylow2blem3  19227  cyggeninv  19483  gsummptnn0fz  19587  dprdff  19615  issubdrg  20049  acsfn1p  20067  cygznlem3  20777  mptcoe1fsupp  21386  cply1coe0bi  21471  gsummoncoe1  21475  scmatdmat  21664  mdetdiagid  21749  mdetunilem9  21769  cpmatmcllem  21867  m2cpminvid2lem  21903  decpmatmulsumfsupp  21922  pmatcollpw1lem1  21923  pmatcollpw2lem  21926  pmatcollpwfi  21931  pm2mpf1  21948  mptcoe1matfsupp  21951  mp2pm2mplem4  21958  pm2mpmhmlem1  21967  pm2mp  21974  chpdmat  21990  chpscmat  21991  cpmidpmatlem3  22021  cayhamlem4  22037  neiptopnei  22283  cncnp  22431  isnrm2  22509  isreg2  22528  2ndcdisj  22607  islly2  22635  dislly  22648  kgen2ss  22706  ptbasfi  22732  ptclsg  22766  prdstopn  22779  txtube  22791  txlm  22799  isr0  22888  filuni  23036  alexsubALTlem3  23200  ptcmplem3  23205  ptcmplem4  23206  tsmsxplem1  23304  prdsmet  23523  metequiv2  23666  metcnpi3  23702  nmoleub  23895  rescncf  24060  cncfco  24070  evth  24122  lebnumlem3  24126  xlebnum  24128  nmoleub2lem2  24279  nmhmcn  24283  lmmcvg  24425  cmetcaulem  24452  caubl  24472  bcth3  24495  ovollb2lem  24652  ovoliunlem2  24667  ovolicc2lem3  24683  ovolicc2lem4  24684  nulmbl2  24700  volsup  24720  ioombl1lem4  24725  dyadmax  24762  vitalilem2  24773  vitalilem5  24776  mbfi1flimlem  24887  itg2seq  24907  itg2addlem  24923  itgcn  25009  limciun  25058  rolle  25154  dvfsumrlim  25195  itgsubst  25213  aannenlem1  25488  aalioulem3  25494  ulmcaulem  25553  ulmcau  25554  ulmss  25556  ulmbdd  25557  ulmcn  25558  ulmdvlem3  25561  mtest  25563  iblulm  25566  itgulm  25567  rlimcnp  26115  xrlimcnp  26118  rlimcxp  26123  o1cxp  26124  amgm  26140  lgambdd  26186  ftalem2  26223  isppw2  26264  mumullem2  26329  2sqlem6  26571  chtppilimlem2  26622  chtppilim  26623  pntrsumbnd2  26715  pntlem3  26757  isperp2  27076  axeuclidlem  27330  axeuclid  27331  uhgrnbgr0nb  27721  vtxdginducedm1fi  27911  cusgrrusgr  27948  rusgrpropnb  27950  rusgrpropedg  27951  rusgrpropadjvtx  27952  upgrewlkle2  27973  wlkvtxiedg  27992  upgrwlkvtxedg  28012  uspgr2wlkeq  28013  redwlk  28040  wlkdlem2  28051  lfgrwlkprop  28055  2pthnloop  28099  upgr2pthnlp  28100  pthdlem1  28134  pthdlem2lem  28135  wlkiswwlks1  28232  wlkiswwlks2lem4  28237  wwlksm1edg  28246  wwlksnred  28257  clwwlkccatlem  28353  clwlkclwwlklem2a  28362  clwlkclwwlklem2  28364  cusconngr  28555  eucrctshift  28607  2pthfrgr  28648  3cyclfrgr  28652  nmoub3i  29135  ubthlem1  29232  ubthlem3  29234  ocsh  29645  chintcli  29693  chscllem2  30000  nmopub2tALT  30271  nmfnleub2  30288  lnconi  30395  riesz1  30427  rnbra  30469  leopadd  30494  leopmuli  30495  leoptr  30499  dmdbr3  30667  dmdbr4  30668  dmdbr5  30670  mdsl0  30672  mdsymlem6  30770  cdj1i  30795  acunirnmpt  30996  xrge0infss  31083  elrspunidl  31606  cmppcmp  31808  zarclsiin  31821  lmxrge0  31902  ftc2re  32578  cvmlift2lem12  33276  nosupbnd1lem5  33915  noinfbnd1lem5  33930  noetasuplem4  33939  noetainflem4  33943  opnrebl2  34510  neibastop1  34548  neibastop2lem  34549  neibastop3  34551  finixpnum  35762  lindsenlbs  35772  matunitlindflem1  35773  matunitlindflem2  35774  ptrecube  35777  poimirlem26  35803  poimirlem27  35804  poimirlem29  35806  poimirlem30  35807  poimir  35810  heicant  35812  itg2addnclem  35828  itg2addnclem3  35830  itg2addnc  35831  filbcmb  35898  nninfnub  35909  geomcau  35917  sstotbnd2  35932  isbndx  35940  prdsbnd  35951  heibor1lem  35967  heiborlem1  35969  heibor  35979  rrncmslem  35990  intidl  36187  pclclN  37905  lauteq  38109  ltrnid  38149  mapdh9a  39803  sticksstones3  40104  fltaccoprm  40477  fltabcoprm  40479  flt4lem5  40487  elrfirn2  40518  isnacs3  40532  rencldnfilem  40642  kelac1  40888  neik0pk1imk0  41657  cvgdvgrat  41931  neglimc  43188  limsupub  43245  limsuppnflem  43251  limsupre3lem  43273  limsupvaluz2  43279  supcnvlimsup  43281  climuzlem  43284  liminfval2  43309  limsupgtlem  43318  liminflelimsupuz  43326  liminflimsupclim  43348  xlimpnfxnegmnf  43355  liminflimsupxrre  43358  xlimmnfv  43375  xlimpnfv  43379  stoweidlem7  43548  fourierdlem73  43720  sge0isum  43965  meaiuninc3v  44022  preimageiingt  44257  preimaleiinlt  44258  smflimlem3  44308  smflimlem4  44309  cfsetsnfsetfo  44554  2reu8i  44605  iccpartres  44870  upwlkwlk  45301  upgrwlkupwlk  45302  copisnmnd  45363  2zrngnmlid2  45509  ply1mulgsumlem1  45727  ply1mulgsumlem3  45729  ply1mulgsumlem4  45730  snlindsntor  45812  eenglngeehlnmlem1  46083  eenglngeehlnmlem2  46084