Theorem exlimdv 1833

Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
exlimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
exlimdv	⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimdv

Step	Hyp	Ref	Expression
1		ax-17 1540	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ax-17 1540	. 2 ⊢ (𝜒 → ∀𝑥𝜒)
3		exlimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	exlimdh 1610	1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1461  ax-gen 1463  ax-ie2 1508  ax-17 1540

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1834  exlimdvv  1912  exlimddv  1913  tpid3g  3738  sssnm  3785  pwntru  4233  euotd  4288  ralxfr2d  4500  rexxfr2d  4501  releldmb  4904  relelrnb  4905  elres  4983  iss  4993  imain  5341  elunirn  5814  ovmpt4g  6046  oprssdmm  6230  op1steq  6238  fo2ndf  6286  reldmtpos  6312  rntpos  6316  tfrlemibacc  6385  tfrlemibxssdm  6386  tfrlemibfn  6387  tfrexlem  6393  tfr1onlembacc  6401  tfr1onlembxssdm  6402  tfr1onlembfn  6403  tfrcllembacc  6414  tfrcllembxssdm  6415  tfrcllembfn  6416  map0g  6748  xpdom3m  6894  phplem4  6917  phpm  6927  findcard2  6951  findcard2s  6952  ac6sfi  6960  fiintim  6993  xpfi  6994  fidcenum  7023  ordiso  7103  ctmlemr  7175  ctm  7176  ctssdc  7180  pm54.43  7259  exmidfodomrlemim  7270  recclnq  7461  ltexnqq  7477  ltbtwnnqq  7484  recexprlemss1l  7704  recexprlemss1u  7705  negm  9691  ioom  10352  seq3f1olemp  10609  fiinfnf1o  10880  fihashf1rn  10882  climcau  11514  summodclem2  11549  zsumdc  11551  isumz  11556  fsumf1o  11557  fisumss  11559  fsumcl2lem  11565  fsumadd  11573  fsummulc2  11615  ntrivcvgap  11715  prodmodclem2  11744  zproddc  11746  prod1dc  11753  fprodf1o  11755  fprodssdc  11757  fprodmul  11758  nnmindc  12211  uzwodc  12214  pceu  12474  4sqlemafi  12574  4sqlem12  12581  ennnfone  12652  enctlem  12659  unct  12669  gsumfzval  13044  sgrpidmndm  13071  subrngintm  13778  subrgintm  13809  islssm  13923  lss0cl  13935  islidlm  14045  eltg3  14303  tgtop  14314  tgidm  14320  tgrest  14415  tgcn  14454  xblm  14663  dvfgg  14934  dvcnp2cntop  14945  2lgslem1  15342  pwtrufal  15652