Theorem ralimdva 3149

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3051

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 1912

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

This theorem is referenced by:  ralimdv  3151  ralimdvva  3184  wereu2  5628  frpomin  6304  fveqressseq  7031  f1mpt  7216  isores3  7290  caofrss  7670  caoftrn  7672  sorpssuni  7686  sorpssint  7687  onint  7744  xpord3inddlem  8104  smogt  8307  fisupg  9198  ixpfi2  9260  fissuni  9267  indexfi  9270  fiinfg  9414  wemaplem2  9462  rankonidlem  9752  ac5num  9958  acni2  9968  acndom2  9976  alephle  10010  dfac5  10051  cfsmolem  10192  isf34lem7  10301  isf34lem6  10302  fin1a2s  10336  acncc  10362  ttukeylem6  10436  fpwwe2lem7  10560  gchina  10622  inar1  10698  tskord  10703  grudomon  10740  grur1a  10742  dedekind  11309  fimaxre  12100  fiminre  12103  uzwo  12861  xrsupsslem  13259  xrinfmsslem  13260  fsuppmapnn0fiub0  13955  rexanre  15309  rexuz3  15311  rexico  15316  cau3lem  15317  limsupval2  15442  rlim2lt  15459  rlim3  15460  lo1bdd2  15486  lo1bddrp  15487  o1lo1  15499  climrlim2  15509  2clim  15534  o1co  15548  rlimcn1  15550  rlimcn3  15552  climcn1  15554  climcn2  15555  subcn2  15557  o1of2  15575  rlimo1  15579  o1rlimmul  15581  lo1add  15589  lo1mul  15590  climsqz  15603  climsqz2  15604  rlimsqzlem  15611  lo1le  15614  climbdd  15634  caucvgrlem  15635  caucvgrlem2  15637  caurcvg2  15640  iseralt  15647  cvgcmp  15779  cvgcmpce  15781  gcdcllem1  16468  absproddvds  16586  coprmprod  16630  coprmproddvdslem  16631  pcfac  16870  pockthg  16877  infpnlem1  16881  prmreclem2  16888  prmreclem3  16889  vdwlem11  16962  vdwlem13  16964  vdwnnlem3  16968  isacs2  17619  acsfn1  17627  acsfn2  17629  catpropd  17675  drsdirfi  18271  ipodrsima  18507  isacs5  18514  mrelatglb  18526  mrelatlub  18528  isgrpinv  18969  dfgrp3e  19016  issubg4  19121  gsmsymgreqlem2  19406  finodsubmsubg  19542  gexdvds  19559  gexcl3  19562  sylow2blem3  19597  cyggeninv  19858  gsummptnn0fz  19961  dprdff  19989  issubdrg  20757  acsfn1p  20776  cygznlem3  21549  psdmul  22132  mptcoe1fsupp  22179  cply1coe0bi  22267  gsummoncoe1  22273  evls1fpws  22334  scmatdmat  22480  mdetdiagid  22565  mdetunilem9  22585  cpmatmcllem  22683  m2cpminvid2lem  22719  decpmatmulsumfsupp  22738  pmatcollpw1lem1  22739  pmatcollpw2lem  22742  pmatcollpwfi  22747  pm2mpf1  22764  mptcoe1matfsupp  22767  mp2pm2mplem4  22774  pm2mpmhmlem1  22783  pm2mp  22790  chpdmat  22806  chpscmat  22807  cpmidpmatlem3  22837  cayhamlem4  22853  neiptopnei  23097  cncnp  23245  isnrm2  23323  isreg2  23342  2ndcdisj  23421  islly2  23449  dislly  23462  kgen2ss  23520  ptbasfi  23546  ptclsg  23580  prdstopn  23593  txtube  23605  txlm  23613  isr0  23702  filuni  23850  alexsubALTlem3  24014  ptcmplem3  24019  ptcmplem4  24020  tsmsxplem1  24118  prdsmet  24335  metequiv2  24475  metcnpi3  24511  nmoleub  24696  rescncf  24864  cncfco  24874  evth  24926  lebnumlem3  24930  xlebnum  24932  nmoleub2lem2  25083  nmhmcn  25087  lmmcvg  25228  cmetcaulem  25255  caubl  25275  bcth3  25298  ovollb2lem  25455  ovoliunlem2  25470  ovolicc2lem3  25486  ovolicc2lem4  25487  nulmbl2  25503  volsup  25523  ioombl1lem4  25528  dyadmax  25565  vitalilem2  25576  vitalilem5  25579  mbfi1flimlem  25689  itg2seq  25709  itg2addlem  25725  itgcn  25812  limciun  25861  rolle  25957  dvfsumrlim  25998  itgsubst  26016  aannenlem1  26294  aalioulem3  26300  ulmcaulem  26359  ulmcau  26360  ulmss  26362  ulmbdd  26363  ulmcn  26364  ulmdvlem3  26367  mtest  26369  iblulm  26372  itgulm  26373  rlimcnp  26929  xrlimcnp  26932  rlimcxp  26937  o1cxp  26938  amgm  26954  lgambdd  27000  ftalem2  27037  isppw2  27078  mumullem2  27143  2sqlem6  27386  chtppilimlem2  27437  chtppilim  27438  pntrsumbnd2  27530  pntlem3  27572  nosupbnd1lem5  27676  noinfbnd1lem5  27691  noetasuplem4  27700  noetainflem4  27704  negbdaylem  28048  mulsuniflem  28141  elreno2  28487  isperp2  28783  axeuclidlem  29031  axeuclid  29032  uhgrnbgr0nb  29423  vtxdginducedm1fi  29613  cusgrrusgr  29650  rusgrpropnb  29652  rusgrpropedg  29653  rusgrpropadjvtx  29654  upgrewlkle2  29675  wlkvtxiedg  29693  upgrwlkvtxedg  29713  uspgr2wlkeq  29714  redwlk  29739  wlkdlem2  29750  lfgrwlkprop  29754  2pthnloop  29799  upgr2pthnlp  29800  pthdlem1  29834  pthdlem2lem  29835  wlkiswwlks1  29935  wlkiswwlks2lem4  29940  wwlksm1edg  29949  wwlksnred  29960  clwwlkccatlem  30059  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  cusconngr  30261  eucrctshift  30313  2pthfrgr  30354  3cyclfrgr  30358  nmoub3i  30844  ubthlem1  30941  ubthlem3  30943  ocsh  31354  chintcli  31402  chscllem2  31709  nmopub2tALT  31980  nmfnleub2  31997  lnconi  32104  riesz1  32136  rnbra  32178  leopadd  32203  leopmuli  32204  leoptr  32208  dmdbr3  32376  dmdbr4  32377  dmdbr5  32379  mdsl0  32381  mdsymlem6  32479  cdj1i  32504  acunirnmpt  32732  xrge0infss  32833  isdrng4  33356  elrspunidl  33488  cmppcmp  34002  zarclsiin  34015  lmxrge0  34096  ftc2re  34742  cvmlift2lem12  35496  opnrebl2  36503  neibastop1  36541  neibastop2lem  36542  neibastop3  36544  finixpnum  37926  lindsenlbs  37936  matunitlindflem1  37937  matunitlindflem2  37938  ptrecube  37941  poimirlem26  37967  poimirlem27  37968  poimirlem29  37970  poimirlem30  37971  poimir  37974  heicant  37976  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  filbcmb  38061  nninfnub  38072  geomcau  38080  sstotbnd2  38095  isbndx  38103  prdsbnd  38114  heibor1lem  38130  heiborlem1  38132  heibor  38142  rrncmslem  38153  intidl  38350  pclclN  40337  lauteq  40541  ltrnid  40581  mapdh9a  42235  primrootscoprmpow  42538  sticksstones3  42587  aks5lem5a  42630  aks5lem6  42631  fltaccoprm  43073  fltabcoprm  43075  flt4lem5  43083  elrfirn2  43128  isnacs3  43142  rencldnfilem  43248  kelac1  43491  naddgeoa  43822  neik0pk1imk0  44474  cvgdvgrat  44740  neglimc  46075  limsupub  46132  limsuppnflem  46138  limsupre3lem  46160  limsupvaluz2  46166  supcnvlimsup  46168  climuzlem  46171  liminfval2  46196  limsupgtlem  46205  liminflelimsupuz  46213  liminflimsupclim  46235  xlimpnfxnegmnf  46242  liminflimsupxrre  46245  xlimmnfv  46262  xlimpnfv  46266  stoweidlem7  46435  fourierdlem73  46607  sge0isum  46855  meaiuninc3v  46912  preimageiingt  47148  preimaleiinlt  47149  smflimlem3  47201  smflimlem4  47202  cfsetsnfsetfo  47508  2reu8i  47561  iccpartres  47878  uhgrimisgrgric  48407  grlictr  48491  clnbgr3stgrgrlim  48495  clnbgr3stgrgrlic  48496  upwlkwlk  48615  upgrwlkupwlk  48616  copisnmnd  48645  2zrngnmlid2  48733  ply1mulgsumlem1  48862  ply1mulgsumlem3  48864  ply1mulgsumlem4  48865  snlindsntor  48947  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  iinfsubc  49533