Theorem exlimdv 1758

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

Syntax hints:   → wi 4  ∃wex 1436

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-5 1391  ax-gen 1393  ax-ie2 1438  ax-17 1474

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v2  1759  exlimdvv  1836  exlimddv  1837  tpid3g  3585  sssnm  3628  euotd  4114  ralxfr2d  4323  rexxfr2d  4324  releldmb  4714  relelrnb  4715  elres  4791  iss  4801  imain  5141  elunirn  5599  ovmpt4g  5825  op1steq  6007  fo2ndf  6054  reldmtpos  6080  rntpos  6084  tfrlemibacc  6153  tfrlemibxssdm  6154  tfrlemibfn  6155  tfrexlem  6161  tfr1onlembacc  6169  tfr1onlembxssdm  6170  tfr1onlembfn  6171  tfrcllembacc  6182  tfrcllembxssdm  6183  tfrcllembfn  6184  map0g  6512  xpdom3m  6657  phplem4  6678  phpm  6688  findcard2  6712  findcard2s  6713  ac6sfi  6721  fiintim  6746  xpfi  6747  fidcenum  6772  ordiso  6836  ctmlemr  6908  ctm  6909  ctssdc  6912  pm54.43  6957  exmidfodomrlemim  6966  recclnq  7101  ltexnqq  7117  ltbtwnnqq  7124  recexprlemss1l  7344  recexprlemss1u  7345  negm  9257  ioom  9879  seq3f1olemp  10116  fiinfnf1o  10373  fihashf1rn  10376  climcau  10955  summodclem2  10990  zsumdc  10992  isumz  10997  fsumf1o  10998  fisumss  11000  fsumcl2lem  11006  fsumadd  11014  fsummulc2  11056  ennnfone  11730  eltg3  12008  tgtop  12019  tgidm  12025  tgrest  12120  tgcn  12158  xblm  12345  dvfgg  12530  pwtrufal  12777  pwntru  12778