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  5907  ovmpt4g  6144  oprssdmm  6334  op1steq  6342  fo2ndf  6392  reldmtpos  6419  rntpos  6423  tfrlemibacc  6492  tfrlemibxssdm  6493  tfrlemibfn  6494  tfrexlem  6500  tfr1onlembacc  6508  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembxssdm  6522  tfrcllembfn  6523  map0g  6857  dom1o  7002  xpdom3m  7018  phplem4  7041  phpm  7052  findcard2  7078  findcard2s  7079  ac6sfi  7087  fiintim  7123  xpfi  7124  fidcenum  7155  ordiso  7235  ctmlemr  7307  ctm  7308  ctssdc  7312  pm54.43  7395  exmidfodomrlemim  7412  iftrueb01  7441  pw1m  7442  recclnq  7612  ltexnqq  7628  ltbtwnnqq  7635  recexprlemss1l  7855  recexprlemss1u  7856  negm  9849  ioom  10521  seq3f1olemp  10778  fiinfnf1o  11049  fihashf1rn  11051  climcau  11912  summodclem2  11948  zsumdc  11950  isumz  11955  fsumf1o  11956  fisumss  11958  fsumcl2lem  11964  fsumadd  11972  fsummulc2  12014  ntrivcvgap  12114  prodmodclem2  12143  zproddc  12145  prod1dc  12152  fprodf1o  12154  fprodssdc  12156  fprodmul  12157  nnmindc  12610  uzwodc  12613  pceu  12873  4sqlemafi  12973  4sqlem12  12980  ennnfone  13051  enctlem  13058  unct  13068  gsumfzval  13479  sgrpidmndm  13508  subrngintm  14232  subrgintm  14263  islssm  14377  lss0cl  14389  islidlm  14499  eltg3  14787  tgtop  14798  tgidm  14804  tgrest  14899  tgcn  14938  xblm  15147  dvfgg  15418  dvcnp2cntop  15429  2lgslem1  15826  pwtrufal  16624  gfsumval  16707