Theorem exlimdv 1833

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

Syntax hints:   → wi 4  ∃wex 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1461  ax-gen 1463  ax-ie2 1508  ax-17 1540

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1834  exlimdvv  1912  exlimddv  1913  tpid3g  3738  sssnm  3785  pwntru  4233  euotd  4288  ralxfr2d  4500  rexxfr2d  4501  releldmb  4904  relelrnb  4905  elres  4983  iss  4993  imain  5341  elunirn  5816  ovmpt4g  6049  oprssdmm  6238  op1steq  6246  fo2ndf  6294  reldmtpos  6320  rntpos  6324  tfrlemibacc  6393  tfrlemibxssdm  6394  tfrlemibfn  6395  tfrexlem  6401  tfr1onlembacc  6409  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfrcllembacc  6422  tfrcllembxssdm  6423  tfrcllembfn  6424  map0g  6756  xpdom3m  6902  phplem4  6925  phpm  6935  findcard2  6959  findcard2s  6960  ac6sfi  6968  fiintim  7001  xpfi  7002  fidcenum  7031  ordiso  7111  ctmlemr  7183  ctm  7184  ctssdc  7188  pm54.43  7269  exmidfodomrlemim  7280  recclnq  7476  ltexnqq  7492  ltbtwnnqq  7499  recexprlemss1l  7719  recexprlemss1u  7720  negm  9706  ioom  10367  seq3f1olemp  10624  fiinfnf1o  10895  fihashf1rn  10897  climcau  11529  summodclem2  11564  zsumdc  11566  isumz  11571  fsumf1o  11572  fisumss  11574  fsumcl2lem  11580  fsumadd  11588  fsummulc2  11630  ntrivcvgap  11730  prodmodclem2  11759  zproddc  11761  prod1dc  11768  fprodf1o  11770  fprodssdc  11772  fprodmul  11773  nnmindc  12226  uzwodc  12229  pceu  12489  4sqlemafi  12589  4sqlem12  12596  ennnfone  12667  enctlem  12674  unct  12684  gsumfzval  13093  sgrpidmndm  13122  subrngintm  13844  subrgintm  13875  islssm  13989  lss0cl  14001  islidlm  14111  eltg3  14377  tgtop  14388  tgidm  14394  tgrest  14489  tgcn  14528  xblm  14737  dvfgg  15008  dvcnp2cntop  15019  2lgslem1  15416  pwtrufal  15728