Theorem exlimdv 1868

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 1575	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ax-17 1575	. 2 ⊢ (𝜒 → ∀𝑥𝜒)
3		exlimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	exlimdh 1645	1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1496  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1869  exlimdvv  1947  exlimddv  1948  tpid3g  3807  sssnm  3858  pwntru  4312  euotd  4371  ralxfr2d  4585  rexxfr2d  4586  reldmm  4975  releldmb  4994  relelrnb  4995  elres  5074  iss  5084  imain  5438  elunirn  5939  ovmpt4g  6176  oprssdmm  6365  op1steq  6373  fo2ndf  6423  reldmtpos  6484  rntpos  6488  tfrlemibacc  6557  tfrlemibxssdm  6558  tfrlemibfn  6559  tfrexlem  6565  tfr1onlembacc  6573  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfrcllembacc  6586  tfrcllembxssdm  6587  tfrcllembfn  6588  map0g  6922  dom1o  7069  xpdom3m  7085  phplem4  7109  phpm  7120  findcard2  7146  findcard2s  7147  ac6sfi  7155  fiintim  7191  xpfi  7192  fidcenum  7226  ordiso  7327  ctmlemr  7399  ctm  7400  ctssdc  7404  pm54.43  7487  exmidfodomrlemim  7504  iftrueb01  7533  pw1m  7534  recclnq  7707  ltexnqq  7723  ltbtwnnqq  7730  recexprlemss1l  7950  recexprlemss1u  7951  negm  9947  ioom  10620  seq3f1olemp  10877  fiinfnf1o  11149  fihashf1rn  11151  climcau  12032  summodclem2  12068  zsumdc  12070  isumz  12075  fsumf1o  12076  fisumss  12078  fsumcl2lem  12084  fsumadd  12092  fsummulc2  12134  ntrivcvgap  12234  prodmodclem2  12263  zproddc  12265  prod1dc  12272  fprodf1o  12274  fprodssdc  12276  fprodmul  12277  nnmindc  12730  uzwodc  12733  pceu  12993  4sqlemafi  13093  4sqlem12  13100  ennnfone  13176  enctlem  13183  unct  13193  gsumfzval  13604  sgrpidmndm  13633  subrngintm  14357  subrgintm  14388  islssm  14505  lss0cl  14517  islidlm  14627  eltg3  14922  tgtop  14933  tgidm  14939  tgrest  15034  tgcn  15073  xblm  15282  dvfgg  15553  dvcnp2cntop  15564  2lgslem1  15964  pwtrufal  16771  gfsumval  16862