Theorem exlimdv 1819

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

Syntax hints:   → wi 4  ∃wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1447  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1820  exlimdvv  1897  exlimddv  1898  tpid3g  3707  sssnm  3754  pwntru  4199  euotd  4254  ralxfr2d  4464  rexxfr2d  4465  releldmb  4864  relelrnb  4865  elres  4943  iss  4953  imain  5298  elunirn  5766  ovmpt4g  5996  oprssdmm  6171  op1steq  6179  fo2ndf  6227  reldmtpos  6253  rntpos  6257  tfrlemibacc  6326  tfrlemibxssdm  6327  tfrlemibfn  6328  tfrexlem  6334  tfr1onlembacc  6342  tfr1onlembxssdm  6343  tfr1onlembfn  6344  tfrcllembacc  6355  tfrcllembxssdm  6356  tfrcllembfn  6357  map0g  6687  xpdom3m  6833  phplem4  6854  phpm  6864  findcard2  6888  findcard2s  6889  ac6sfi  6897  fiintim  6927  xpfi  6928  fidcenum  6954  ordiso  7034  ctmlemr  7106  ctm  7107  ctssdc  7111  pm54.43  7188  exmidfodomrlemim  7199  recclnq  7390  ltexnqq  7406  ltbtwnnqq  7413  recexprlemss1l  7633  recexprlemss1u  7634  negm  9614  ioom  10260  seq3f1olemp  10501  fiinfnf1o  10765  fihashf1rn  10767  climcau  11354  summodclem2  11389  zsumdc  11391  isumz  11396  fsumf1o  11397  fisumss  11399  fsumcl2lem  11405  fsumadd  11413  fsummulc2  11455  ntrivcvgap  11555  prodmodclem2  11584  zproddc  11586  prod1dc  11593  fprodf1o  11595  fprodssdc  11597  fprodmul  11598  nnmindc  12034  uzwodc  12037  pceu  12294  ennnfone  12425  enctlem  12432  unct  12442  sgrpidmndm  12820  subrgintm  13362  eltg3  13527  tgtop  13538  tgidm  13544  tgrest  13639  tgcn  13678  xblm  13887  dvfgg  14127  dvcnp2cntop  14133  pwtrufal  14717