Theorem eximdv 1742

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
alimdv.1	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
eximdv	⊢ (φ → (∃xψ → ∃xχ))

Distinct variable group:   φ,x

Allowed substitution hints:   ψ(x)   χ(x)

Proof of Theorem eximdv

Step	Hyp	Ref	Expression
1		ax-17 1400	. 2 ⊢ (φ → ∀xφ)
2		alimdv.1	. 2 ⊢ (φ → (ψ → χ))
3	1, 2	eximdh 1484	1 ⊢ (φ → (∃xψ → ∃xχ))

Syntax hints:   → wi 4  ∃wex 1362

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2eximdv  1744  reximdv2  2396  cgsexg  2566  spc3egv  2621  euind  2705  ssel  2916  reupick  3198  reximdva0m  3213  uniss  3575  eusvnfb  4136  coss1  4418  coss2  4419  dmss  4461  dmcosseq  4530  funssres  4868  imain  4907  brprcneu  5096  fv3  5122  dffo4  5240  dffo5  5241  f1eqcocnv  5356  dmaddpq  6238  dmmulpq  6239  recexprlemlol  6460  recexprlemupu  6462