Theorem exlimdv 1867

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

Syntax hints:   → wi 4  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1496  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1868  exlimdvv  1946  exlimddv  1947  tpid3g  3791  sssnm  3842  pwntru  4295  euotd  4353  ralxfr2d  4567  rexxfr2d  4568  reldmm  4956  releldmb  4975  relelrnb  4976  elres  5055  iss  5065  imain  5419  elunirn  5917  ovmpt4g  6154  oprssdmm  6343  op1steq  6351  fo2ndf  6401  reldmtpos  6462  rntpos  6466  tfrlemibacc  6535  tfrlemibxssdm  6536  tfrlemibfn  6537  tfrexlem  6543  tfr1onlembacc  6551  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfrcllembacc  6564  tfrcllembxssdm  6565  tfrcllembfn  6566  map0g  6900  dom1o  7045  xpdom3m  7061  phplem4  7084  phpm  7095  findcard2  7121  findcard2s  7122  ac6sfi  7130  fiintim  7166  xpfi  7167  fidcenum  7198  ordiso  7278  ctmlemr  7350  ctm  7351  ctssdc  7355  pm54.43  7438  exmidfodomrlemim  7455  iftrueb01  7484  pw1m  7485  recclnq  7655  ltexnqq  7671  ltbtwnnqq  7678  recexprlemss1l  7898  recexprlemss1u  7899  negm  9893  ioom  10566  seq3f1olemp  10823  fiinfnf1o  11094  fihashf1rn  11096  climcau  11970  summodclem2  12006  zsumdc  12008  isumz  12013  fsumf1o  12014  fisumss  12016  fsumcl2lem  12022  fsumadd  12030  fsummulc2  12072  ntrivcvgap  12172  prodmodclem2  12201  zproddc  12203  prod1dc  12210  fprodf1o  12212  fprodssdc  12214  fprodmul  12215  nnmindc  12668  uzwodc  12671  pceu  12931  4sqlemafi  13031  4sqlem12  13038  ennnfone  13109  enctlem  13116  unct  13126  gsumfzval  13537  sgrpidmndm  13566  subrngintm  14290  subrgintm  14321  islssm  14436  lss0cl  14448  islidlm  14558  eltg3  14851  tgtop  14862  tgidm  14868  tgrest  14963  tgcn  15002  xblm  15211  dvfgg  15482  dvcnp2cntop  15493  2lgslem1  15893  pwtrufal  16702  gfsumval  16792