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  3785  sssnm  3835  pwntru  4287  euotd  4345  ralxfr2d  4559  rexxfr2d  4560  reldmm  4948  releldmb  4967  relelrnb  4968  elres  5047  iss  5057  imain  5409  elunirn  5902  ovmpt4g  6139  oprssdmm  6329  op1steq  6337  fo2ndf  6387  reldmtpos  6414  rntpos  6418  tfrlemibacc  6487  tfrlemibxssdm  6488  tfrlemibfn  6489  tfrexlem  6495  tfr1onlembacc  6503  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfrcllembacc  6516  tfrcllembxssdm  6517  tfrcllembfn  6518  map0g  6852  dom1o  6997  xpdom3m  7013  phplem4  7036  phpm  7047  findcard2  7071  findcard2s  7072  ac6sfi  7080  fiintim  7116  xpfi  7117  fidcenum  7146  ordiso  7226  ctmlemr  7298  ctm  7299  ctssdc  7303  pm54.43  7386  exmidfodomrlemim  7402  iftrueb01  7431  pw1m  7432  recclnq  7602  ltexnqq  7618  ltbtwnnqq  7625  recexprlemss1l  7845  recexprlemss1u  7846  negm  9839  ioom  10510  seq3f1olemp  10767  fiinfnf1o  11038  fihashf1rn  11040  climcau  11898  summodclem2  11933  zsumdc  11935  isumz  11940  fsumf1o  11941  fisumss  11943  fsumcl2lem  11949  fsumadd  11957  fsummulc2  11999  ntrivcvgap  12099  prodmodclem2  12128  zproddc  12130  prod1dc  12137  fprodf1o  12139  fprodssdc  12141  fprodmul  12142  nnmindc  12595  uzwodc  12598  pceu  12858  4sqlemafi  12958  4sqlem12  12965  ennnfone  13036  enctlem  13043  unct  13053  gsumfzval  13464  sgrpidmndm  13493  subrngintm  14216  subrgintm  14247  islssm  14361  lss0cl  14373  islidlm  14483  eltg3  14771  tgtop  14782  tgidm  14788  tgrest  14883  tgcn  14922  xblm  15131  dvfgg  15402  dvcnp2cntop  15413  2lgslem1  15810  pwtrufal  16534