Theorem ralimdva 3146

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3049

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3050

This theorem is referenced by:  ralimdv  3148  ralimdvva  3181  wereu2  5619  frpomin  6296  fveqressseq  7022  f1mpt  7205  isores3  7279  caofrss  7659  caoftrn  7661  sorpssuni  7675  sorpssint  7676  onint  7733  xpord3inddlem  8094  smogt  8297  fisupg  9186  ixpfi2  9248  fissuni  9255  indexfi  9258  fiinfg  9402  wemaplem2  9450  rankonidlem  9738  ac5num  9944  acni2  9954  acndom2  9962  alephle  9996  dfac5  10037  cfsmolem  10178  isf34lem7  10287  isf34lem6  10288  fin1a2s  10322  acncc  10348  ttukeylem6  10422  fpwwe2lem7  10546  gchina  10608  inar1  10684  tskord  10689  grudomon  10726  grur1a  10728  dedekind  11294  fimaxre  12084  fiminre  12087  uzwo  12822  xrsupsslem  13220  xrinfmsslem  13221  fsuppmapnn0fiub0  13914  rexanre  15268  rexuz3  15270  rexico  15275  cau3lem  15276  limsupval2  15401  rlim2lt  15418  rlim3  15419  lo1bdd2  15445  lo1bddrp  15446  o1lo1  15458  climrlim2  15468  2clim  15493  o1co  15507  rlimcn1  15509  rlimcn3  15511  climcn1  15513  climcn2  15514  subcn2  15516  o1of2  15534  rlimo1  15538  o1rlimmul  15540  lo1add  15548  lo1mul  15549  climsqz  15562  climsqz2  15563  rlimsqzlem  15570  lo1le  15573  climbdd  15593  caucvgrlem  15594  caucvgrlem2  15596  caurcvg2  15599  iseralt  15606  cvgcmp  15737  cvgcmpce  15739  gcdcllem1  16424  absproddvds  16542  coprmprod  16586  coprmproddvdslem  16587  pcfac  16825  pockthg  16832  infpnlem1  16836  prmreclem2  16843  prmreclem3  16844  vdwlem11  16917  vdwlem13  16919  vdwnnlem3  16923  isacs2  17574  acsfn1  17582  acsfn2  17584  catpropd  17630  drsdirfi  18226  ipodrsima  18462  isacs5  18469  mrelatglb  18481  mrelatlub  18483  isgrpinv  18921  dfgrp3e  18968  issubg4  19073  gsmsymgreqlem2  19358  finodsubmsubg  19494  gexdvds  19511  gexcl3  19514  sylow2blem3  19549  cyggeninv  19810  gsummptnn0fz  19913  dprdff  19941  issubdrg  20711  acsfn1p  20730  cygznlem3  21522  psdmul  22107  mptcoe1fsupp  22154  cply1coe0bi  22244  gsummoncoe1  22250  evls1fpws  22311  scmatdmat  22457  mdetdiagid  22542  mdetunilem9  22562  cpmatmcllem  22660  m2cpminvid2lem  22696  decpmatmulsumfsupp  22715  pmatcollpw1lem1  22716  pmatcollpw2lem  22719  pmatcollpwfi  22724  pm2mpf1  22741  mptcoe1matfsupp  22744  mp2pm2mplem4  22751  pm2mpmhmlem1  22760  pm2mp  22767  chpdmat  22783  chpscmat  22784  cpmidpmatlem3  22814  cayhamlem4  22830  neiptopnei  23074  cncnp  23222  isnrm2  23300  isreg2  23319  2ndcdisj  23398  islly2  23426  dislly  23439  kgen2ss  23497  ptbasfi  23523  ptclsg  23557  prdstopn  23570  txtube  23582  txlm  23590  isr0  23679  filuni  23827  alexsubALTlem3  23991  ptcmplem3  23996  ptcmplem4  23997  tsmsxplem1  24095  prdsmet  24312  metequiv2  24452  metcnpi3  24488  nmoleub  24673  rescncf  24844  cncfco  24854  evth  24912  lebnumlem3  24916  xlebnum  24918  nmoleub2lem2  25070  nmhmcn  25074  lmmcvg  25215  cmetcaulem  25242  caubl  25262  bcth3  25285  ovollb2lem  25443  ovoliunlem2  25458  ovolicc2lem3  25474  ovolicc2lem4  25475  nulmbl2  25491  volsup  25511  ioombl1lem4  25516  dyadmax  25553  vitalilem2  25564  vitalilem5  25567  mbfi1flimlem  25677  itg2seq  25697  itg2addlem  25713  itgcn  25800  limciun  25849  rolle  25948  dvfsumrlim  25992  itgsubst  26010  aannenlem1  26290  aalioulem3  26296  ulmcaulem  26357  ulmcau  26358  ulmss  26360  ulmbdd  26361  ulmcn  26362  ulmdvlem3  26365  mtest  26367  iblulm  26370  itgulm  26371  rlimcnp  26929  xrlimcnp  26932  rlimcxp  26938  o1cxp  26939  amgm  26955  lgambdd  27001  ftalem2  27038  isppw2  27079  mumullem2  27144  2sqlem6  27388  chtppilimlem2  27439  chtppilim  27440  pntrsumbnd2  27532  pntlem3  27574  nosupbnd1lem5  27678  noinfbnd1lem5  27693  noetasuplem4  27702  noetainflem4  27706  negsbdaylem  28025  mulsuniflem  28118  elreno2  28440  isperp2  28736  axeuclidlem  28984  axeuclid  28985  uhgrnbgr0nb  29376  vtxdginducedm1fi  29567  cusgrrusgr  29604  rusgrpropnb  29606  rusgrpropedg  29607  rusgrpropadjvtx  29608  upgrewlkle2  29629  wlkvtxiedg  29647  upgrwlkvtxedg  29667  uspgr2wlkeq  29668  redwlk  29693  wlkdlem2  29704  lfgrwlkprop  29708  2pthnloop  29753  upgr2pthnlp  29754  pthdlem1  29788  pthdlem2lem  29789  wlkiswwlks1  29889  wlkiswwlks2lem4  29894  wwlksm1edg  29903  wwlksnred  29914  clwwlkccatlem  30013  clwlkclwwlklem2a  30022  clwlkclwwlklem2  30024  cusconngr  30215  eucrctshift  30267  2pthfrgr  30308  3cyclfrgr  30312  nmoub3i  30797  ubthlem1  30894  ubthlem3  30896  ocsh  31307  chintcli  31355  chscllem2  31662  nmopub2tALT  31933  nmfnleub2  31950  lnconi  32057  riesz1  32089  rnbra  32131  leopadd  32156  leopmuli  32157  leoptr  32161  dmdbr3  32329  dmdbr4  32330  dmdbr5  32332  mdsl0  32334  mdsymlem6  32432  cdj1i  32457  acunirnmpt  32686  xrge0infss  32789  isdrng4  33326  elrspunidl  33458  cmppcmp  33964  zarclsiin  33977  lmxrge0  34058  ftc2re  34704  cvmlift2lem12  35457  opnrebl2  36464  neibastop1  36502  neibastop2lem  36503  neibastop3  36505  finixpnum  37745  lindsenlbs  37755  matunitlindflem1  37756  matunitlindflem2  37757  ptrecube  37760  poimirlem26  37786  poimirlem27  37787  poimirlem29  37789  poimirlem30  37790  poimir  37793  heicant  37795  itg2addnclem  37811  itg2addnclem3  37813  itg2addnc  37814  filbcmb  37880  nninfnub  37891  geomcau  37899  sstotbnd2  37914  isbndx  37922  prdsbnd  37933  heibor1lem  37949  heiborlem1  37951  heibor  37961  rrncmslem  37972  intidl  38169  pclclN  40090  lauteq  40294  ltrnid  40334  mapdh9a  41988  primrootscoprmpow  42292  sticksstones3  42341  aks5lem5a  42384  aks5lem6  42385  fltaccoprm  42825  fltabcoprm  42827  flt4lem5  42835  elrfirn2  42880  isnacs3  42894  rencldnfilem  43004  kelac1  43247  naddgeoa  43578  neik0pk1imk0  44230  cvgdvgrat  44496  neglimc  45833  limsupub  45890  limsuppnflem  45896  limsupre3lem  45918  limsupvaluz2  45924  supcnvlimsup  45926  climuzlem  45929  liminfval2  45954  limsupgtlem  45963  liminflelimsupuz  45971  liminflimsupclim  45993  xlimpnfxnegmnf  46000  liminflimsupxrre  46003  xlimmnfv  46020  xlimpnfv  46024  stoweidlem7  46193  fourierdlem73  46365  sge0isum  46613  meaiuninc3v  46670  preimageiingt  46906  preimaleiinlt  46907  smflimlem3  46959  smflimlem4  46960  cfsetsnfsetfo  47248  2reu8i  47301  iccpartres  47606  uhgrimisgrgric  48119  grlictr  48203  clnbgr3stgrgrlim  48207  clnbgr3stgrgrlic  48208  upwlkwlk  48327  upgrwlkupwlk  48328  copisnmnd  48357  2zrngnmlid2  48445  ply1mulgsumlem1  48574  ply1mulgsumlem3  48576  ply1mulgsumlem4  48577  snlindsntor  48659  eenglngeehlnmlem1  48925  eenglngeehlnmlem2  48926  iinfsubc  49245