Theorem exlimdv 1807

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

Syntax hints:   → wi 4  ∃wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1435  ax-gen 1437  ax-ie2 1482  ax-17 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v2  1808  exlimdvv  1885  exlimddv  1886  tpid3g  3691  sssnm  3734  pwntru  4178  euotd  4232  ralxfr2d  4442  rexxfr2d  4443  releldmb  4841  relelrnb  4842  elres  4920  iss  4930  imain  5270  elunirn  5734  ovmpt4g  5964  oprssdmm  6139  op1steq  6147  fo2ndf  6195  reldmtpos  6221  rntpos  6225  tfrlemibacc  6294  tfrlemibxssdm  6295  tfrlemibfn  6296  tfrexlem  6302  tfr1onlembacc  6310  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfrcllembacc  6323  tfrcllembxssdm  6324  tfrcllembfn  6325  map0g  6654  xpdom3m  6800  phplem4  6821  phpm  6831  findcard2  6855  findcard2s  6856  ac6sfi  6864  fiintim  6894  xpfi  6895  fidcenum  6921  ordiso  7001  ctmlemr  7073  ctm  7074  ctssdc  7078  pm54.43  7146  exmidfodomrlemim  7157  recclnq  7333  ltexnqq  7349  ltbtwnnqq  7356  recexprlemss1l  7576  recexprlemss1u  7577  negm  9553  ioom  10196  seq3f1olemp  10437  fiinfnf1o  10699  fihashf1rn  10702  climcau  11288  summodclem2  11323  zsumdc  11325  isumz  11330  fsumf1o  11331  fisumss  11333  fsumcl2lem  11339  fsumadd  11347  fsummulc2  11389  ntrivcvgap  11489  prodmodclem2  11518  zproddc  11520  prod1dc  11527  fprodf1o  11529  fprodssdc  11531  fprodmul  11532  nnmindc  11967  uzwodc  11970  pceu  12227  ennnfone  12358  enctlem  12365  unct  12375  eltg3  12697  tgtop  12708  tgidm  12714  tgrest  12809  tgcn  12848  xblm  13057  dvfgg  13297  dvcnp2cntop  13303  pwtrufal  13877