Theorem ralimdva 3175

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3078

This theorem is used by:  ralimdv  3177  ralimdvva  3210  wereu2  5648  frpomin  6343  fveqressseq  7079  f1mpt  7265  isores3  7343  caofrss  7732  caoftrn  7734  sorpssuni  7748  sorpssint  7749  onint  7804  xpord3inddlem  8171  smogt  8375  fisupg  9279  ixpfi2  9339  fissuni  9346  indexfi  9349  fiinfg  9493  wemaplem2  9541  rankonidlem  9838  ac5num  10115  acni2  10125  acndom2  10133  alephle  10167  dfac5  10207  cfsmolem  10348  isf34lem7  10457  isf34lem6  10458  fin1a2s  10492  acncc  10518  ttukeylem6  10592  fpwwe2lem7  10722  gchina  10784  inar1  10860  tskord  10865  grudomon  10902  grur1a  10904  dedekind  11473  fimaxre  12261  fiminre  12264  uzwo  13038  xrsupsslem  13437  xrinfmsslem  13438  fsuppmapnn0fiub0  14136  rexanre  15514  rexuz3  15516  rexico  15521  cau3lem  15522  limsupval2  15647  rlim2lt  15664  rlim3  15665  lo1bdd2  15691  lo1bddrp  15692  o1lo1  15704  climrlim2  15714  2clim  15739  o1co  15753  rlimcn1  15755  rlimcn3  15757  climcn1  15759  climcn2  15760  subcn2  15762  o1of2  15780  rlimo1  15784  o1rlimmul  15786  lo1add  15794  lo1mul  15795  climsqz  15808  climsqz2  15809  rlimsqzlem  15816  lo1le  15819  climbdd  15839  caucvgrlem  15840  caucvgrlem2  15842  caurcvg2  15845  iseralt  15852  cvgcmp  15983  cvgcmpce  15985  gcdcllem1  16669  absproddvds  16792  coprmprod  16836  coprmproddvdslem  16837  pcfac  17077  pockthg  17084  infpnlem1  17088  prmreclem2  17095  prmreclem3  17096  vdwlem11  17169  vdwlem13  17171  vdwnnlem3  17175  isacs2  17827  acsfn1  17835  acsfn2  17837  catpropd  17883  drsdirfi  18479  ipodrsima  18715  isacs5  18722  mrelatglb  18734  mrelatlub  18736  isgrpinv  19204  dfgrp3e  19250  issubg4  19356  gsmsymgreqlem2  19645  finodsubmsubg  19781  gexdvds  19798  gexcl3  19801  sylow2blem3  19836  cyggeninv  20097  gsummptnn0fz  20200  dprdff  20228  isdrng4  20992  issubdrg  21037  acsfn1p  21056  cygznlem3  21875  lindsenlbs  22157  psdmul  22487  mptcoe1fsupp  22533  cply1coe0bi  22620  gsummoncoe1  22626  evls1fpws  22687  scmatdmat  22830  mdetdiagid  22915  mdetunilem9  22935  matunitlindflem1  22994  matunitlindflem2  22995  cpmatmcllem  23036  m2cpminvid2lem  23072  decpmatmulsumfsupp  23091  pmatcollpw1lem1  23092  pmatcollpw2lem  23095  pmatcollpwfi  23100  pm2mpf1  23117  mptcoe1matfsupp  23120  mp2pm2mplem4  23127  pm2mpmhmlem1  23136  pm2mp  23143  chpdmat  23159  chpscmat  23160  cpmidpmatlem3  23190  cayhamlem4  23206  neiptopnei  23450  cncnp  23598  isnrm2  23676  isreg2  23695  2ndcdisj  23775  islly2  23803  dislly  23816  kgen2ss  23874  ptbasfi  23900  ptclsg  23934  prdstopn  23947  txtube  23959  txlm  23967  isr0  24056  filuni  24204  alexsubALTlem3  24368  ptcmplem3  24373  ptcmplem4  24374  tsmsxplem1  24472  prdsmet  24689  metequiv2  24829  metcnpi3  24865  nmoleub  25050  rescncf  25218  cncfco  25228  evth  25280  lebnumlem3  25284  xlebnum  25286  nmoleub2lem2  25437  nmhmcn  25441  lmmcvg  25582  cmetcaulem  25609  caubl  25629  bcth3  25652  ovollb2lem  25809  ovoliunlem2  25824  ovolicc2lem3  25840  ovolicc2lem4  25841  nulmbl2  25857  volsup  25877  ioombl1lem4  25882  dyadmax  25919  vitalilem2  25930  vitalilem5  25933  mbfi1flimlem  26043  itg2seq  26063  itg2addlem  26079  itgcn  26165  limciun  26214  rolle  26310  dvfsumrlim  26351  itgsubst  26369  aannenlem1  26655  aalioulem3  26661  ulmcaulem  26721  ulmcau  26722  ulmss  26724  ulmbdd  26725  ulmcn  26726  ulmdvlem3  26729  mtest  26731  iblulm  26734  itgulm  26735  rlimcnp  27293  xrlimcnp  27296  rlimcxp  27301  o1cxp  27302  amgm  27318  lgambdd  27364  ftalem2  27401  isppw2  27442  mumullem2  27507  2sqlem6  27750  chtppilimlem2  27801  chtppilim  27802  pntrsumbnd2  27894  pntlem3  27936  fltaccoprm  27972  fltabcoprm  27974  flt4lem5  27980  nosupbnd1lem5  28069  noinfbnd1lem5  28084  noetasuplem4  28093  noetainflem4  28097  negbdaylem  28442  mulsuniflem  28535  elreno2  28881  isperp2  29190  axeuclidlem  29540  axeuclid  29541  uhgrnbgr0nb  29935  vtxdginducedm1fi  30125  cusgrrusgr  30162  rusgrpropnb  30164  rusgrpropedg  30165  rusgrpropadjvtx  30166  upgrewlkle2  30187  wlkvtxiedg  30205  upgrwlkvtxedg  30225  uspgr2wlkeq  30226  redwlk  30251  wlkdlem2  30262  lfgrwlkprop  30270  2pthnloop  30317  upgr2pthnlp  30318  pthdlem1  30352  pthdlem2lem  30353  wlkiswwlks1  30456  wlkiswwlks2lem4  30461  wwlksm1edg  30470  wwlksnred  30481  clwwlkccatlem  30580  clwlkclwwlklem2a  30589  clwlkclwwlklem2  30591  cusconngr  30792  eucrctshift  30844  2pthfrgr  30885  3cyclfrgr  30889  nmoub3i  31375  ubthlem1  31472  ubthlem3  31474  ocsh  31885  chintcli  31933  chscllem2  32240  nmopub2tALT  32511  nmfnleub2  32528  lnconi  32635  riesz1  32667  rnbra  32709  leopadd  32734  leopmuli  32735  leoptr  32739  dmdbr3  32907  dmdbr4  32908  dmdbr5  32910  mdsl0  32912  mdsymlem6  33010  cdj1i  33035  acunirnmpt  33253  xrge0infss  33352  elrspunidl  33978  dflring2  34025  cmppcmp  34490  zarclsiin  34503  lmxrge0  34584  ftc2re  35227  cvmlift2lem12  36079  nmulrid  36946  opnrebl2  37109  neibastop1  37147  neibastop2lem  37148  neibastop3  37150  finixpnum  38528  ptrecube  38538  poimirlem26  38564  poimirlem27  38565  poimirlem29  38567  poimirlem30  38568  poimir  38571  heicant  38573  itg2addnclem  38589  itg2addnclem3  38591  itg2addnc  38592  filbcmb  38674  nninfnub  38685  geomcau  38693  sstotbnd2  38708  isbndx  38716  prdsbnd  38727  heibor1lem  38743  heiborlem1  38745  heibor  38755  rrncmslem  38766  intidl  38963  pclclN  40948  lauteq  41152  ltrnid  41192  mapdh9a  42846  primrootscoprmpow  43149  sticksstones3  43198  aks5lem5a  43241  aks5lem6  43242  elrfirn2  43706  isnacs3  43720  rencldnfilem  43826  kelac1  44064  naddgeoa  44395  neik0pk1imk0  45046  cvgdvgrat  45296  neglimc  46656  limsupub  46713  limsuppnflem  46719  limsupre3lem  46741  limsupvaluz2  46747  supcnvlimsup  46749  climuzlem  46752  liminfval2  46777  limsupgtlem  46786  liminflelimsupuz  46794  liminflimsupclim  46816  xlimpnfxnegmnf  46823  liminflimsupxrre  46826  xlimmnfv  46843  xlimpnfv  46847  stoweidlem7  47016  fourierdlem73  47188  sge0isum  47436  meaiuninc3v  47493  preimageiingt  47729  preimaleiinlt  47730  smflimlem3  47782  smflimlem4  47783  cfsetsnfsetfo  48129  2reu8i  48182  iccpartres  48499  uhgrimisgrgric  49028  grlictr  49112  clnbgr3stgrgrlim  49116  clnbgr3stgrgrlic  49117  upwlkwlk  49236  upgrwlkupwlk  49237  copisnmnd  49265  2zrngnmlid2  49353  ply1mulgsumlem1  49497  ply1mulgsumlem3  49499  ply1mulgsumlem4  49500  snlindsntor  49582  eenglngeehlnmlem1  49848  eenglngeehlnmlem2  49849  iinfsubc  50165