Theorem exlimdv 1806

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

Syntax hints:   → wi 4  ∃wex 1479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1434  ax-gen 1436  ax-ie2 1481  ax-17 1513

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v2  1807  exlimdvv  1884  exlimddv  1885  tpid3g  3685  sssnm  3728  pwntru  4172  euotd  4226  ralxfr2d  4436  rexxfr2d  4437  releldmb  4835  relelrnb  4836  elres  4914  iss  4924  imain  5264  elunirn  5728  ovmpt4g  5955  oprssdmm  6131  op1steq  6139  fo2ndf  6186  reldmtpos  6212  rntpos  6216  tfrlemibacc  6285  tfrlemibxssdm  6286  tfrlemibfn  6287  tfrexlem  6293  tfr1onlembacc  6301  tfr1onlembxssdm  6302  tfr1onlembfn  6303  tfrcllembacc  6314  tfrcllembxssdm  6315  tfrcllembfn  6316  map0g  6645  xpdom3m  6791  phplem4  6812  phpm  6822  findcard2  6846  findcard2s  6847  ac6sfi  6855  fiintim  6885  xpfi  6886  fidcenum  6912  ordiso  6992  ctmlemr  7064  ctm  7065  ctssdc  7069  pm54.43  7137  exmidfodomrlemim  7148  recclnq  7324  ltexnqq  7340  ltbtwnnqq  7347  recexprlemss1l  7567  recexprlemss1u  7568  negm  9544  ioom  10186  seq3f1olemp  10427  fiinfnf1o  10688  fihashf1rn  10691  climcau  11274  summodclem2  11309  zsumdc  11311  isumz  11316  fsumf1o  11317  fisumss  11319  fsumcl2lem  11325  fsumadd  11333  fsummulc2  11375  ntrivcvgap  11475  prodmodclem2  11504  zproddc  11506  prod1dc  11513  fprodf1o  11515  fprodssdc  11517  fprodmul  11518  pceu  12204  ennnfone  12295  enctlem  12302  unct  12312  nnmindc  12318  eltg3  12598  tgtop  12609  tgidm  12615  tgrest  12710  tgcn  12749  xblm  12958  dvfgg  13198  dvcnp2cntop  13204  pwtrufal  13711