Theorem exlimdv 1744

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

Syntax hints:   → wi 4  ∃wex 1424

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-5 1379  ax-gen 1381  ax-ie2 1426  ax-17 1462

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ax11v2  1745  exlimdvv  1822  exlimddv  1823  tpid3g  3537  sssnm  3580  euotd  4053  ralxfr2d  4258  rexxfr2d  4259  releldmb  4638  relelrnb  4639  elres  4713  iss  4723  imain  5057  elunirn  5499  ovmpt4g  5717  op1steq  5899  fo2ndf  5942  reldmtpos  5965  rntpos  5969  tfrlemibacc  6038  tfrlemibxssdm  6039  tfrlemibfn  6040  tfrexlem  6046  tfr1onlembacc  6054  tfr1onlembxssdm  6055  tfr1onlembfn  6056  tfrcllembacc  6067  tfrcllembxssdm  6068  tfrcllembfn  6069  map0g  6390  xpdom3m  6495  phplem4  6516  phpm  6526  findcard2  6550  findcard2s  6551  ac6sfi  6559  xpfi  6583  ordiso  6665  pm54.43  6754  exmidfodomrlemim  6763  recclnq  6887  ltexnqq  6903  ltbtwnnqq  6910  recexprlemss1l  7130  recexprlemss1u  7131  negm  9024  ioom  9592  iseqf1olemp  9827  fiinfnf1o  10082  fihashf1rn  10085  climcau  10618  isummolem2  10653  zisum  10655  isumz  10659  fsumf1o  10660