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  3781  sssnm  3831  pwntru  4282  euotd  4340  ralxfr2d  4554  rexxfr2d  4555  reldmm  4941  releldmb  4960  relelrnb  4961  elres  5040  iss  5050  imain  5402  elunirn  5889  ovmpt4g  6126  oprssdmm  6315  op1steq  6323  fo2ndf  6371  reldmtpos  6397  rntpos  6401  tfrlemibacc  6470  tfrlemibxssdm  6471  tfrlemibfn  6472  tfrexlem  6478  tfr1onlembacc  6486  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfrcllembacc  6499  tfrcllembxssdm  6500  tfrcllembfn  6501  map0g  6833  xpdom3m  6989  phplem4  7012  phpm  7023  findcard2  7047  findcard2s  7048  ac6sfi  7056  fiintim  7089  xpfi  7090  fidcenum  7119  ordiso  7199  ctmlemr  7271  ctm  7272  ctssdc  7276  pm54.43  7359  exmidfodomrlemim  7375  iftrueb01  7404  pw1m  7405  recclnq  7575  ltexnqq  7591  ltbtwnnqq  7598  recexprlemss1l  7818  recexprlemss1u  7819  negm  9806  ioom  10475  seq3f1olemp  10732  fiinfnf1o  11003  fihashf1rn  11005  climcau  11853  summodclem2  11888  zsumdc  11890  isumz  11895  fsumf1o  11896  fisumss  11898  fsumcl2lem  11904  fsumadd  11912  fsummulc2  11954  ntrivcvgap  12054  prodmodclem2  12083  zproddc  12085  prod1dc  12092  fprodf1o  12094  fprodssdc  12096  fprodmul  12097  nnmindc  12550  uzwodc  12553  pceu  12813  4sqlemafi  12913  4sqlem12  12920  ennnfone  12991  enctlem  12998  unct  13008  gsumfzval  13419  sgrpidmndm  13448  subrngintm  14170  subrgintm  14201  islssm  14315  lss0cl  14327  islidlm  14437  eltg3  14725  tgtop  14736  tgidm  14742  tgrest  14837  tgcn  14876  xblm  15085  dvfgg  15356  dvcnp2cntop  15367  2lgslem1  15764  dom1o  16314  pwtrufal  16322