Theorem ralimdva 3102

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 3101	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

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

This theorem is referenced by:  ralimdv  3103  ralimdvva  3104  wereu2  5577  frpomin  6228  fveqressseq  6939  f1mpt  7115  isores3  7186  caofrss  7547  caoftrn  7549  sorpssuni  7563  sorpssint  7564  onint  7617  smogt  8169  fisupg  8992  ixpfi2  9047  fissuni  9054  indexfi  9057  fiinfg  9188  wemaplem2  9236  rankonidlem  9517  ac5num  9723  acni2  9733  acndom2  9741  alephle  9775  dfac5  9815  cfsmolem  9957  isf34lem7  10066  isf34lem6  10067  fin1a2s  10101  acncc  10127  ttukeylem6  10201  fpwwe2lem7  10324  gchina  10386  inar1  10462  tskord  10467  grudomon  10504  grur1a  10506  dedekind  11068  fimaxre  11849  fiminre  11852  uzwo  12580  xrsupsslem  12970  xrinfmsslem  12971  fsuppmapnn0fiub0  13641  rexanre  14986  rexuz3  14988  rexico  14993  cau3lem  14994  limsupval2  15117  rlim2lt  15134  rlim3  15135  lo1bdd2  15161  lo1bddrp  15162  o1lo1  15174  climrlim2  15184  2clim  15209  o1co  15223  rlimcn1  15225  rlimcn3  15227  climcn1  15229  climcn2  15230  subcn2  15232  o1of2  15250  rlimo1  15254  o1rlimmul  15256  lo1add  15264  lo1mul  15265  climsqz  15278  climsqz2  15279  rlimsqzlem  15288  lo1le  15291  climbdd  15311  caucvgrlem  15312  caucvgrlem2  15314  caurcvg2  15317  iseralt  15324  cvgcmp  15456  cvgcmpce  15458  gcdcllem1  16134  absproddvds  16250  coprmprod  16294  coprmproddvdslem  16295  pcfac  16528  pockthg  16535  infpnlem1  16539  prmreclem2  16546  prmreclem3  16547  vdwlem11  16620  vdwlem13  16622  vdwnnlem3  16626  isacs2  17279  acsfn1  17287  acsfn2  17289  catpropd  17335  drsdirfi  17938  ipodrsima  18174  isacs5  18181  mrelatglb  18193  mrelatlub  18195  isgrpinv  18547  dfgrp3e  18590  issubg4  18689  gsmsymgreqlem2  18954  gexdvds  19104  gexcl3  19107  sylow2blem3  19142  cyggeninv  19398  gsummptnn0fz  19502  dprdff  19530  issubdrg  19964  acsfn1p  19982  cygznlem3  20689  mptcoe1fsupp  21296  cply1coe0bi  21381  gsummoncoe1  21385  scmatdmat  21572  mdetdiagid  21657  mdetunilem9  21677  cpmatmcllem  21775  m2cpminvid2lem  21811  decpmatmulsumfsupp  21830  pmatcollpw1lem1  21831  pmatcollpw2lem  21834  pmatcollpwfi  21839  pm2mpf1  21856  mptcoe1matfsupp  21859  mp2pm2mplem4  21866  pm2mpmhmlem1  21875  pm2mp  21882  chpdmat  21898  chpscmat  21899  cpmidpmatlem3  21929  cayhamlem4  21945  neiptopnei  22191  cncnp  22339  isnrm2  22417  isreg2  22436  2ndcdisj  22515  islly2  22543  dislly  22556  kgen2ss  22614  ptbasfi  22640  ptclsg  22674  prdstopn  22687  txtube  22699  txlm  22707  isr0  22796  filuni  22944  alexsubALTlem3  23108  ptcmplem3  23113  ptcmplem4  23114  tsmsxplem1  23212  prdsmet  23431  metequiv2  23572  metcnpi3  23608  nmoleub  23801  rescncf  23966  cncfco  23976  evth  24028  lebnumlem3  24032  xlebnum  24034  nmoleub2lem2  24185  nmhmcn  24189  lmmcvg  24330  cmetcaulem  24357  caubl  24377  bcth3  24400  ovollb2lem  24557  ovoliunlem2  24572  ovolicc2lem3  24588  ovolicc2lem4  24589  nulmbl2  24605  volsup  24625  ioombl1lem4  24630  dyadmax  24667  vitalilem2  24678  vitalilem5  24681  mbfi1flimlem  24792  itg2seq  24812  itg2addlem  24828  itgcn  24914  limciun  24963  rolle  25059  dvfsumrlim  25100  itgsubst  25118  aannenlem1  25393  aalioulem3  25399  ulmcaulem  25458  ulmcau  25459  ulmss  25461  ulmbdd  25462  ulmcn  25463  ulmdvlem3  25466  mtest  25468  iblulm  25471  itgulm  25472  rlimcnp  26020  xrlimcnp  26023  rlimcxp  26028  o1cxp  26029  amgm  26045  lgambdd  26091  ftalem2  26128  isppw2  26169  mumullem2  26234  2sqlem6  26476  chtppilimlem2  26527  chtppilim  26528  pntrsumbnd2  26620  pntlem3  26662  isperp2  26980  axeuclidlem  27233  axeuclid  27234  uhgrnbgr0nb  27624  vtxdginducedm1fi  27814  cusgrrusgr  27851  rusgrpropnb  27853  rusgrpropedg  27854  rusgrpropadjvtx  27855  upgrewlkle2  27876  wlkvtxiedg  27894  upgrwlkvtxedg  27914  uspgr2wlkeq  27915  redwlk  27942  wlkdlem2  27953  lfgrwlkprop  27957  2pthnloop  28000  upgr2pthnlp  28001  pthdlem1  28035  pthdlem2lem  28036  wlkiswwlks1  28133  wlkiswwlks2lem4  28138  wwlksm1edg  28147  wwlksnred  28158  clwwlkccatlem  28254  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  cusconngr  28456  eucrctshift  28508  2pthfrgr  28549  3cyclfrgr  28553  nmoub3i  29036  ubthlem1  29133  ubthlem3  29135  ocsh  29546  chintcli  29594  chscllem2  29901  nmopub2tALT  30172  nmfnleub2  30189  lnconi  30296  riesz1  30328  rnbra  30370  leopadd  30395  leopmuli  30396  leoptr  30400  dmdbr3  30568  dmdbr4  30569  dmdbr5  30571  mdsl0  30573  mdsymlem6  30671  cdj1i  30696  acunirnmpt  30898  xrge0infss  30985  elrspunidl  31508  cmppcmp  31710  zarclsiin  31723  lmxrge0  31804  ftc2re  32478  cvmlift2lem12  33176  nosupbnd1lem5  33842  noinfbnd1lem5  33857  noetasuplem4  33866  noetainflem4  33870  opnrebl2  34437  neibastop1  34475  neibastop2lem  34476  neibastop3  34478  finixpnum  35689  lindsenlbs  35699  matunitlindflem1  35700  matunitlindflem2  35701  ptrecube  35704  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  poimirlem30  35734  poimir  35737  heicant  35739  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  filbcmb  35825  nninfnub  35836  geomcau  35844  sstotbnd2  35859  isbndx  35867  prdsbnd  35878  heibor1lem  35894  heiborlem1  35896  heibor  35906  rrncmslem  35917  intidl  36114  pclclN  37832  lauteq  38036  ltrnid  38076  mapdh9a  39730  sticksstones3  40032  fltaccoprm  40393  fltabcoprm  40395  flt4lem5  40403  elrfirn2  40434  isnacs3  40448  rencldnfilem  40558  kelac1  40804  neik0pk1imk0  41546  cvgdvgrat  41820  neglimc  43078  limsupub  43135  limsuppnflem  43141  limsupre3lem  43163  limsupvaluz2  43169  supcnvlimsup  43171  climuzlem  43174  liminfval2  43199  limsupgtlem  43208  liminflelimsupuz  43216  liminflimsupclim  43238  xlimpnfxnegmnf  43245  liminflimsupxrre  43248  xlimmnfv  43265  xlimpnfv  43269  stoweidlem7  43438  fourierdlem73  43610  sge0isum  43855  meaiuninc3v  43912  preimageiingt  44144  preimaleiinlt  44145  smflimlem3  44195  smflimlem4  44196  cfsetsnfsetfo  44441  2reu8i  44492  iccpartres  44758  upwlkwlk  45189  upgrwlkupwlk  45190  copisnmnd  45251  2zrngnmlid2  45397  ply1mulgsumlem1  45615  ply1mulgsumlem3  45617  ply1mulgsumlem4  45618  snlindsntor  45700  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972