Theorem exlimdv 1830

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

Syntax hints:   → wi 4  ∃wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1458  ax-gen 1460  ax-ie2 1505  ax-17 1537

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1831  exlimdvv  1909  exlimddv  1910  tpid3g  3722  sssnm  3769  pwntru  4214  euotd  4269  ralxfr2d  4479  rexxfr2d  4480  releldmb  4879  relelrnb  4880  elres  4958  iss  4968  imain  5314  elunirn  5784  ovmpt4g  6015  oprssdmm  6191  op1steq  6199  fo2ndf  6247  reldmtpos  6273  rntpos  6277  tfrlemibacc  6346  tfrlemibxssdm  6347  tfrlemibfn  6348  tfrexlem  6354  tfr1onlembacc  6362  tfr1onlembxssdm  6363  tfr1onlembfn  6364  tfrcllembacc  6375  tfrcllembxssdm  6376  tfrcllembfn  6377  map0g  6709  xpdom3m  6855  phplem4  6878  phpm  6888  findcard2  6912  findcard2s  6913  ac6sfi  6921  fiintim  6952  xpfi  6953  fidcenum  6980  ordiso  7060  ctmlemr  7132  ctm  7133  ctssdc  7137  pm54.43  7214  exmidfodomrlemim  7225  recclnq  7416  ltexnqq  7432  ltbtwnnqq  7439  recexprlemss1l  7659  recexprlemss1u  7660  negm  9640  ioom  10286  seq3f1olemp  10528  fiinfnf1o  10793  fihashf1rn  10795  climcau  11382  summodclem2  11417  zsumdc  11419  isumz  11424  fsumf1o  11425  fisumss  11427  fsumcl2lem  11433  fsumadd  11441  fsummulc2  11483  ntrivcvgap  11583  prodmodclem2  11612  zproddc  11614  prod1dc  11621  fprodf1o  11623  fprodssdc  11625  fprodmul  11626  nnmindc  12062  uzwodc  12065  pceu  12322  4sqlemafi  12422  4sqlem12  12429  ennnfone  12471  enctlem  12478  unct  12488  sgrpidmndm  12874  subrngintm  13552  subrgintm  13583  islssm  13666  lss0cl  13678  islidlm  13788  eltg3  13994  tgtop  14005  tgidm  14011  tgrest  14106  tgcn  14145  xblm  14354  dvfgg  14594  dvcnp2cntop  14600  pwtrufal  15185