Theorem ralimdva 3168

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062

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 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  ralimdv  3170  ralimdvva  3205  wereu2  5674  frpomin  6342  fveqressseq  7082  f1mpt  7260  isores3  7332  caofrss  7706  caoftrn  7708  sorpssuni  7722  sorpssint  7723  onint  7778  xpord3inddlem  8140  smogt  8367  fisupg  9291  ixpfi2  9350  fissuni  9357  indexfi  9360  fiinfg  9494  wemaplem2  9542  rankonidlem  9823  ac5num  10031  acni2  10041  acndom2  10049  alephle  10083  dfac5  10123  cfsmolem  10265  isf34lem7  10374  isf34lem6  10375  fin1a2s  10409  acncc  10435  ttukeylem6  10509  fpwwe2lem7  10632  gchina  10694  inar1  10770  tskord  10775  grudomon  10812  grur1a  10814  dedekind  11377  fimaxre  12158  fiminre  12161  uzwo  12895  xrsupsslem  13286  xrinfmsslem  13287  fsuppmapnn0fiub0  13958  rexanre  15293  rexuz3  15295  rexico  15300  cau3lem  15301  limsupval2  15424  rlim2lt  15441  rlim3  15442  lo1bdd2  15468  lo1bddrp  15469  o1lo1  15481  climrlim2  15491  2clim  15516  o1co  15530  rlimcn1  15532  rlimcn3  15534  climcn1  15536  climcn2  15537  subcn2  15539  o1of2  15557  rlimo1  15561  o1rlimmul  15563  lo1add  15571  lo1mul  15572  climsqz  15585  climsqz2  15586  rlimsqzlem  15595  lo1le  15598  climbdd  15618  caucvgrlem  15619  caucvgrlem2  15621  caurcvg2  15624  iseralt  15631  cvgcmp  15762  cvgcmpce  15764  gcdcllem1  16440  absproddvds  16554  coprmprod  16598  coprmproddvdslem  16599  pcfac  16832  pockthg  16839  infpnlem1  16843  prmreclem2  16850  prmreclem3  16851  vdwlem11  16924  vdwlem13  16926  vdwnnlem3  16930  isacs2  17597  acsfn1  17605  acsfn2  17607  catpropd  17653  drsdirfi  18258  ipodrsima  18494  isacs5  18501  mrelatglb  18513  mrelatlub  18515  isgrpinv  18878  dfgrp3e  18923  issubg4  19025  gsmsymgreqlem2  19299  finodsubmsubg  19435  gexdvds  19452  gexcl3  19455  sylow2blem3  19490  cyggeninv  19751  gsummptnn0fz  19854  dprdff  19882  issubdrg  20401  acsfn1p  20415  cygznlem3  21125  mptcoe1fsupp  21739  cply1coe0bi  21824  gsummoncoe1  21828  scmatdmat  22017  mdetdiagid  22102  mdetunilem9  22122  cpmatmcllem  22220  m2cpminvid2lem  22256  decpmatmulsumfsupp  22275  pmatcollpw1lem1  22276  pmatcollpw2lem  22279  pmatcollpwfi  22284  pm2mpf1  22301  mptcoe1matfsupp  22304  mp2pm2mplem4  22311  pm2mpmhmlem1  22320  pm2mp  22327  chpdmat  22343  chpscmat  22344  cpmidpmatlem3  22374  cayhamlem4  22390  neiptopnei  22636  cncnp  22784  isnrm2  22862  isreg2  22881  2ndcdisj  22960  islly2  22988  dislly  23001  kgen2ss  23059  ptbasfi  23085  ptclsg  23119  prdstopn  23132  txtube  23144  txlm  23152  isr0  23241  filuni  23389  alexsubALTlem3  23553  ptcmplem3  23558  ptcmplem4  23559  tsmsxplem1  23657  prdsmet  23876  metequiv2  24019  metcnpi3  24055  nmoleub  24248  rescncf  24413  cncfco  24423  evth  24475  lebnumlem3  24479  xlebnum  24481  nmoleub2lem2  24632  nmhmcn  24636  lmmcvg  24778  cmetcaulem  24805  caubl  24825  bcth3  24848  ovollb2lem  25005  ovoliunlem2  25020  ovolicc2lem3  25036  ovolicc2lem4  25037  nulmbl2  25053  volsup  25073  ioombl1lem4  25078  dyadmax  25115  vitalilem2  25126  vitalilem5  25129  mbfi1flimlem  25240  itg2seq  25260  itg2addlem  25276  itgcn  25362  limciun  25411  rolle  25507  dvfsumrlim  25548  itgsubst  25566  aannenlem1  25841  aalioulem3  25847  ulmcaulem  25906  ulmcau  25907  ulmss  25909  ulmbdd  25910  ulmcn  25911  ulmdvlem3  25914  mtest  25916  iblulm  25919  itgulm  25920  rlimcnp  26470  xrlimcnp  26473  rlimcxp  26478  o1cxp  26479  amgm  26495  lgambdd  26541  ftalem2  26578  isppw2  26619  mumullem2  26684  2sqlem6  26926  chtppilimlem2  26977  chtppilim  26978  pntrsumbnd2  27070  pntlem3  27112  nosupbnd1lem5  27215  noinfbnd1lem5  27230  noetasuplem4  27239  noetainflem4  27243  negsbdaylem  27530  mulsuniflem  27604  isperp2  27966  axeuclidlem  28220  axeuclid  28221  uhgrnbgr0nb  28611  vtxdginducedm1fi  28801  cusgrrusgr  28838  rusgrpropnb  28840  rusgrpropedg  28841  rusgrpropadjvtx  28842  upgrewlkle2  28863  wlkvtxiedg  28882  upgrwlkvtxedg  28902  uspgr2wlkeq  28903  redwlk  28929  wlkdlem2  28940  lfgrwlkprop  28944  2pthnloop  28988  upgr2pthnlp  28989  pthdlem1  29023  pthdlem2lem  29024  wlkiswwlks1  29121  wlkiswwlks2lem4  29126  wwlksm1edg  29135  wwlksnred  29146  clwwlkccatlem  29242  clwlkclwwlklem2a  29251  clwlkclwwlklem2  29253  cusconngr  29444  eucrctshift  29496  2pthfrgr  29537  3cyclfrgr  29541  nmoub3i  30026  ubthlem1  30123  ubthlem3  30125  ocsh  30536  chintcli  30584  chscllem2  30891  nmopub2tALT  31162  nmfnleub2  31179  lnconi  31286  riesz1  31318  rnbra  31360  leopadd  31385  leopmuli  31386  leoptr  31390  dmdbr3  31558  dmdbr4  31559  dmdbr5  31561  mdsl0  31563  mdsymlem6  31661  cdj1i  31686  acunirnmpt  31884  xrge0infss  31973  isdrng4  32395  elrspunidl  32546  evls1fpws  32646  cmppcmp  32838  zarclsiin  32851  lmxrge0  32932  ftc2re  33610  cvmlift2lem12  34305  opnrebl2  35206  neibastop1  35244  neibastop2lem  35245  neibastop3  35247  finixpnum  36473  lindsenlbs  36483  matunitlindflem1  36484  matunitlindflem2  36485  ptrecube  36488  poimirlem26  36514  poimirlem27  36515  poimirlem29  36517  poimirlem30  36518  poimir  36521  heicant  36523  itg2addnclem  36539  itg2addnclem3  36541  itg2addnc  36542  filbcmb  36608  nninfnub  36619  geomcau  36627  sstotbnd2  36642  isbndx  36650  prdsbnd  36661  heibor1lem  36677  heiborlem1  36679  heibor  36689  rrncmslem  36700  intidl  36897  pclclN  38762  lauteq  38966  ltrnid  39006  mapdh9a  40660  sticksstones3  40964  fltaccoprm  41382  fltabcoprm  41384  flt4lem5  41392  elrfirn2  41434  isnacs3  41448  rencldnfilem  41558  kelac1  41805  naddgeoa  42145  neik0pk1imk0  42798  cvgdvgrat  43072  neglimc  44363  limsupub  44420  limsuppnflem  44426  limsupre3lem  44448  limsupvaluz2  44454  supcnvlimsup  44456  climuzlem  44459  liminfval2  44484  limsupgtlem  44493  liminflelimsupuz  44501  liminflimsupclim  44523  xlimpnfxnegmnf  44530  liminflimsupxrre  44533  xlimmnfv  44550  xlimpnfv  44554  stoweidlem7  44723  fourierdlem73  44895  sge0isum  45143  meaiuninc3v  45200  preimageiingt  45436  preimaleiinlt  45437  smflimlem3  45489  smflimlem4  45490  cfsetsnfsetfo  45770  2reu8i  45821  iccpartres  46086  upwlkwlk  46517  upgrwlkupwlk  46518  copisnmnd  46579  2zrngnmlid2  46849  ply1mulgsumlem1  47067  ply1mulgsumlem3  47069  ply1mulgsumlem4  47070  snlindsntor  47152  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424