Theorem exlimdv 1865

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

Syntax hints:   → wi 4  ∃wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1493  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1866  exlimdvv  1944  exlimddv  1945  tpid3g  3782  sssnm  3832  pwntru  4283  euotd  4341  ralxfr2d  4555  rexxfr2d  4556  reldmm  4942  releldmb  4961  relelrnb  4962  elres  5041  iss  5051  imain  5403  elunirn  5896  ovmpt4g  6133  oprssdmm  6323  op1steq  6331  fo2ndf  6379  reldmtpos  6405  rntpos  6409  tfrlemibacc  6478  tfrlemibxssdm  6479  tfrlemibfn  6480  tfrexlem  6486  tfr1onlembacc  6494  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfrcllembacc  6507  tfrcllembxssdm  6508  tfrcllembfn  6509  map0g  6843  dom1o  6985  xpdom3m  7001  phplem4  7024  phpm  7035  findcard2  7059  findcard2s  7060  ac6sfi  7068  fiintim  7104  xpfi  7105  fidcenum  7134  ordiso  7214  ctmlemr  7286  ctm  7287  ctssdc  7291  pm54.43  7374  exmidfodomrlemim  7390  iftrueb01  7419  pw1m  7420  recclnq  7590  ltexnqq  7606  ltbtwnnqq  7613  recexprlemss1l  7833  recexprlemss1u  7834  negm  9822  ioom  10492  seq3f1olemp  10749  fiinfnf1o  11020  fihashf1rn  11022  climcau  11873  summodclem2  11908  zsumdc  11910  isumz  11915  fsumf1o  11916  fisumss  11918  fsumcl2lem  11924  fsumadd  11932  fsummulc2  11974  ntrivcvgap  12074  prodmodclem2  12103  zproddc  12105  prod1dc  12112  fprodf1o  12114  fprodssdc  12116  fprodmul  12117  nnmindc  12570  uzwodc  12573  pceu  12833  4sqlemafi  12933  4sqlem12  12940  ennnfone  13011  enctlem  13018  unct  13028  gsumfzval  13439  sgrpidmndm  13468  subrngintm  14191  subrgintm  14222  islssm  14336  lss0cl  14348  islidlm  14458  eltg3  14746  tgtop  14757  tgidm  14763  tgrest  14858  tgcn  14897  xblm  15106  dvfgg  15377  dvcnp2cntop  15388  2lgslem1  15785  pwtrufal  16422