Theorem exlimdv 1817

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

Syntax hints:   → wi 4  ∃wex 1490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1445  ax-gen 1447  ax-ie2 1492  ax-17 1524

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1818  exlimdvv  1895  exlimddv  1896  tpid3g  3704  sssnm  3750  pwntru  4194  euotd  4248  ralxfr2d  4458  rexxfr2d  4459  releldmb  4857  relelrnb  4858  elres  4936  iss  4946  imain  5290  elunirn  5757  ovmpt4g  5987  oprssdmm  6162  op1steq  6170  fo2ndf  6218  reldmtpos  6244  rntpos  6248  tfrlemibacc  6317  tfrlemibxssdm  6318  tfrlemibfn  6319  tfrexlem  6325  tfr1onlembacc  6333  tfr1onlembxssdm  6334  tfr1onlembfn  6335  tfrcllembacc  6346  tfrcllembxssdm  6347  tfrcllembfn  6348  map0g  6678  xpdom3m  6824  phplem4  6845  phpm  6855  findcard2  6879  findcard2s  6880  ac6sfi  6888  fiintim  6918  xpfi  6919  fidcenum  6945  ordiso  7025  ctmlemr  7097  ctm  7098  ctssdc  7102  pm54.43  7179  exmidfodomrlemim  7190  recclnq  7366  ltexnqq  7382  ltbtwnnqq  7389  recexprlemss1l  7609  recexprlemss1u  7610  negm  9588  ioom  10231  seq3f1olemp  10472  fiinfnf1o  10734  fihashf1rn  10736  climcau  11323  summodclem2  11358  zsumdc  11360  isumz  11365  fsumf1o  11366  fisumss  11368  fsumcl2lem  11374  fsumadd  11382  fsummulc2  11424  ntrivcvgap  11524  prodmodclem2  11553  zproddc  11555  prod1dc  11562  fprodf1o  11564  fprodssdc  11566  fprodmul  11567  nnmindc  12002  uzwodc  12005  pceu  12262  ennnfone  12393  enctlem  12400  unct  12410  sgrpidmndm  12696  eltg3  13137  tgtop  13148  tgidm  13154  tgrest  13249  tgcn  13288  xblm  13497  dvfgg  13737  dvcnp2cntop  13743  pwtrufal  14316