Theorem ralimdva 3160

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

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

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

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

This theorem is referenced by:  ralimdv  3162  ralimdvva  3197  wereu2  5635  frpomin  6299  fveqressseq  7035  f1mpt  7213  isores3  7285  caofrss  7658  caoftrn  7660  sorpssuni  7674  sorpssint  7675  onint  7730  xpord3inddlem  8091  smogt  8318  fisupg  9242  ixpfi2  9301  fissuni  9308  indexfi  9311  fiinfg  9444  wemaplem2  9492  rankonidlem  9773  ac5num  9981  acni2  9991  acndom2  9999  alephle  10033  dfac5  10073  cfsmolem  10215  isf34lem7  10324  isf34lem6  10325  fin1a2s  10359  acncc  10385  ttukeylem6  10459  fpwwe2lem7  10582  gchina  10644  inar1  10720  tskord  10725  grudomon  10762  grur1a  10764  dedekind  11327  fimaxre  12108  fiminre  12111  uzwo  12845  xrsupsslem  13236  xrinfmsslem  13237  fsuppmapnn0fiub0  13908  rexanre  15243  rexuz3  15245  rexico  15250  cau3lem  15251  limsupval2  15374  rlim2lt  15391  rlim3  15392  lo1bdd2  15418  lo1bddrp  15419  o1lo1  15431  climrlim2  15441  2clim  15466  o1co  15480  rlimcn1  15482  rlimcn3  15484  climcn1  15486  climcn2  15487  subcn2  15489  o1of2  15507  rlimo1  15511  o1rlimmul  15513  lo1add  15521  lo1mul  15522  climsqz  15535  climsqz2  15536  rlimsqzlem  15545  lo1le  15548  climbdd  15568  caucvgrlem  15569  caucvgrlem2  15571  caurcvg2  15574  iseralt  15581  cvgcmp  15712  cvgcmpce  15714  gcdcllem1  16390  absproddvds  16504  coprmprod  16548  coprmproddvdslem  16549  pcfac  16782  pockthg  16789  infpnlem1  16793  prmreclem2  16800  prmreclem3  16801  vdwlem11  16874  vdwlem13  16876  vdwnnlem3  16880  isacs2  17547  acsfn1  17555  acsfn2  17557  catpropd  17603  drsdirfi  18208  ipodrsima  18444  isacs5  18451  mrelatglb  18463  mrelatlub  18465  isgrpinv  18818  dfgrp3e  18861  issubg4  18961  gsmsymgreqlem2  19227  finodsubmsubg  19363  gexdvds  19380  gexcl3  19383  sylow2blem3  19418  cyggeninv  19674  gsummptnn0fz  19777  dprdff  19805  issubdrg  20296  acsfn1p  20322  cygznlem3  21013  mptcoe1fsupp  21623  cply1coe0bi  21708  gsummoncoe1  21712  scmatdmat  21901  mdetdiagid  21986  mdetunilem9  22006  cpmatmcllem  22104  m2cpminvid2lem  22140  decpmatmulsumfsupp  22159  pmatcollpw1lem1  22160  pmatcollpw2lem  22163  pmatcollpwfi  22168  pm2mpf1  22185  mptcoe1matfsupp  22188  mp2pm2mplem4  22195  pm2mpmhmlem1  22204  pm2mp  22211  chpdmat  22227  chpscmat  22228  cpmidpmatlem3  22258  cayhamlem4  22274  neiptopnei  22520  cncnp  22668  isnrm2  22746  isreg2  22765  2ndcdisj  22844  islly2  22872  dislly  22885  kgen2ss  22943  ptbasfi  22969  ptclsg  23003  prdstopn  23016  txtube  23028  txlm  23036  isr0  23125  filuni  23273  alexsubALTlem3  23437  ptcmplem3  23442  ptcmplem4  23443  tsmsxplem1  23541  prdsmet  23760  metequiv2  23903  metcnpi3  23939  nmoleub  24132  rescncf  24297  cncfco  24307  evth  24359  lebnumlem3  24363  xlebnum  24365  nmoleub2lem2  24516  nmhmcn  24520  lmmcvg  24662  cmetcaulem  24689  caubl  24709  bcth3  24732  ovollb2lem  24889  ovoliunlem2  24904  ovolicc2lem3  24920  ovolicc2lem4  24921  nulmbl2  24937  volsup  24957  ioombl1lem4  24962  dyadmax  24999  vitalilem2  25010  vitalilem5  25013  mbfi1flimlem  25124  itg2seq  25144  itg2addlem  25160  itgcn  25246  limciun  25295  rolle  25391  dvfsumrlim  25432  itgsubst  25450  aannenlem1  25725  aalioulem3  25731  ulmcaulem  25790  ulmcau  25791  ulmss  25793  ulmbdd  25794  ulmcn  25795  ulmdvlem3  25798  mtest  25800  iblulm  25803  itgulm  25804  rlimcnp  26352  xrlimcnp  26355  rlimcxp  26360  o1cxp  26361  amgm  26377  lgambdd  26423  ftalem2  26460  isppw2  26501  mumullem2  26566  2sqlem6  26808  chtppilimlem2  26859  chtppilim  26860  pntrsumbnd2  26952  pntlem3  26994  nosupbnd1lem5  27097  noinfbnd1lem5  27112  noetasuplem4  27121  noetainflem4  27125  isperp2  27720  axeuclidlem  27974  axeuclid  27975  uhgrnbgr0nb  28365  vtxdginducedm1fi  28555  cusgrrusgr  28592  rusgrpropnb  28594  rusgrpropedg  28595  rusgrpropadjvtx  28596  upgrewlkle2  28617  wlkvtxiedg  28636  upgrwlkvtxedg  28656  uspgr2wlkeq  28657  redwlk  28683  wlkdlem2  28694  lfgrwlkprop  28698  2pthnloop  28742  upgr2pthnlp  28743  pthdlem1  28777  pthdlem2lem  28778  wlkiswwlks1  28875  wlkiswwlks2lem4  28880  wwlksm1edg  28889  wwlksnred  28900  clwwlkccatlem  28996  clwlkclwwlklem2a  29005  clwlkclwwlklem2  29007  cusconngr  29198  eucrctshift  29250  2pthfrgr  29291  3cyclfrgr  29295  nmoub3i  29778  ubthlem1  29875  ubthlem3  29877  ocsh  30288  chintcli  30336  chscllem2  30643  nmopub2tALT  30914  nmfnleub2  30931  lnconi  31038  riesz1  31070  rnbra  31112  leopadd  31137  leopmuli  31138  leoptr  31142  dmdbr3  31310  dmdbr4  31311  dmdbr5  31313  mdsl0  31315  mdsymlem6  31413  cdj1i  31438  acunirnmpt  31642  xrge0infss  31733  elrspunidl  32279  evls1fpws  32348  cmppcmp  32528  zarclsiin  32541  lmxrge0  32622  ftc2re  33300  cvmlift2lem12  33995  opnrebl2  34869  neibastop1  34907  neibastop2lem  34908  neibastop3  34910  finixpnum  36136  lindsenlbs  36146  matunitlindflem1  36147  matunitlindflem2  36148  ptrecube  36151  poimirlem26  36177  poimirlem27  36178  poimirlem29  36180  poimirlem30  36181  poimir  36184  heicant  36186  itg2addnclem  36202  itg2addnclem3  36204  itg2addnc  36205  filbcmb  36272  nninfnub  36283  geomcau  36291  sstotbnd2  36306  isbndx  36314  prdsbnd  36325  heibor1lem  36341  heiborlem1  36343  heibor  36353  rrncmslem  36364  intidl  36561  pclclN  38427  lauteq  38631  ltrnid  38671  mapdh9a  40325  sticksstones3  40629  fltaccoprm  41036  fltabcoprm  41038  flt4lem5  41046  elrfirn2  41077  isnacs3  41091  rencldnfilem  41201  kelac1  41448  naddgeoa  41788  neik0pk1imk0  42441  cvgdvgrat  42715  neglimc  44008  limsupub  44065  limsuppnflem  44071  limsupre3lem  44093  limsupvaluz2  44099  supcnvlimsup  44101  climuzlem  44104  liminfval2  44129  limsupgtlem  44138  liminflelimsupuz  44146  liminflimsupclim  44168  xlimpnfxnegmnf  44175  liminflimsupxrre  44178  xlimmnfv  44195  xlimpnfv  44199  stoweidlem7  44368  fourierdlem73  44540  sge0isum  44788  meaiuninc3v  44845  preimageiingt  45081  preimaleiinlt  45082  smflimlem3  45134  smflimlem4  45135  cfsetsnfsetfo  45414  2reu8i  45465  iccpartres  45730  upwlkwlk  46161  upgrwlkupwlk  46162  copisnmnd  46223  2zrngnmlid2  46369  ply1mulgsumlem1  46587  ply1mulgsumlem3  46589  ply1mulgsumlem4  46590  snlindsntor  46672  eenglngeehlnmlem1  46943  eenglngeehlnmlem2  46944