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

Syntax hints:   → wi 4  ∃wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1495  ax-gen 1497  ax-ie2 1542  ax-17 1574

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1868  exlimdvv  1946  exlimddv  1947  tpid3g  3787  sssnm  3837  pwntru  4289  euotd  4347  ralxfr2d  4561  rexxfr2d  4562  reldmm  4950  releldmb  4969  relelrnb  4970  elres  5049  iss  5059  imain  5412  elunirn  5906  ovmpt4g  6143  oprssdmm  6333  op1steq  6341  fo2ndf  6391  reldmtpos  6418  rntpos  6422  tfrlemibacc  6491  tfrlemibxssdm  6492  tfrlemibfn  6493  tfrexlem  6499  tfr1onlembacc  6507  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfrcllembacc  6520  tfrcllembxssdm  6521  tfrcllembfn  6522  map0g  6856  dom1o  7001  xpdom3m  7017  phplem4  7040  phpm  7051  findcard2  7077  findcard2s  7078  ac6sfi  7086  fiintim  7122  xpfi  7123  fidcenum  7154  ordiso  7234  ctmlemr  7306  ctm  7307  ctssdc  7311  pm54.43  7394  exmidfodomrlemim  7411  iftrueb01  7440  pw1m  7441  recclnq  7611  ltexnqq  7627  ltbtwnnqq  7634  recexprlemss1l  7854  recexprlemss1u  7855  negm  9848  ioom  10519  seq3f1olemp  10776  fiinfnf1o  11047  fihashf1rn  11049  climcau  11907  summodclem2  11942  zsumdc  11944  isumz  11949  fsumf1o  11950  fisumss  11952  fsumcl2lem  11958  fsumadd  11966  fsummulc2  12008  ntrivcvgap  12108  prodmodclem2  12137  zproddc  12139  prod1dc  12146  fprodf1o  12148  fprodssdc  12150  fprodmul  12151  nnmindc  12604  uzwodc  12607  pceu  12867  4sqlemafi  12967  4sqlem12  12974  ennnfone  13045  enctlem  13052  unct  13062  gsumfzval  13473  sgrpidmndm  13502  subrngintm  14225  subrgintm  14256  islssm  14370  lss0cl  14382  islidlm  14492  eltg3  14780  tgtop  14791  tgidm  14797  tgrest  14892  tgcn  14931  xblm  15140  dvfgg  15411  dvcnp2cntop  15422  2lgslem1  15819  pwtrufal  16598  gfsumval  16680