Theorem exlimdv 1740

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

Syntax hints:   → wi 4  ∃wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-5 1376  ax-gen 1378  ax-ie2 1423  ax-17 1459

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ax11v2  1741  exlimdvv  1818  exlimddv  1819  tpid3g  3505  sssnm  3546  euotd  4009  ralxfr2d  4214  rexxfr2d  4215  releldmb  4589  relelrnb  4590  elres  4664  iss  4674  imain  5001  elunirn  5426  ovmpt4g  5643  op1steq  5825  fo2ndf  5868  reldmtpos  5891  rntpos  5895  tfrlemibacc  5963  tfrlemibxssdm  5964  tfrlemibfn  5965  tfrexlem  5971  freccl  6016  xpdom3m  6331  phplem4  6341  phpm  6351  findcard2  6373  findcard2s  6374  ac6sfi  6379  ordiso  6447  pm54.43  6459  recclnq  6582  ltexnqq  6598  ltbtwnnqq  6605  recexprlemss1l  6825  recexprlemss1u  6826  negm  8700  ioom  9269  climcau  10184