Theorem eximdv 1757

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 1416	. 2 ⊢ (φ → ∀xφ)
2		alimdv.1	. 2 ⊢ (φ → (ψ → χ))
3	1, 2	eximdh 1499	1 ⊢ (φ → (∃xψ → ∃xχ))

Syntax hints:   → wi 4  ∃wex 1378

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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2eximdv  1759  reximdv2  2412  cgsexg  2583  spc3egv  2638  euind  2722  ssel  2933  reupick  3215  reximdva0m  3230  uniss  3592  eusvnfb  4152  coss1  4434  coss2  4435  dmss  4477  dmcosseq  4546  funssres  4885  imain  4924  brprcneu  5114  fv3  5140  dffo4  5258  dffo5  5259  f1eqcocnv  5374  dmaddpq  6363  dmmulpq  6364  recexprlemlol  6597  recexprlemupu  6599