Theorem eximdv 1880

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	⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem eximdv

Step	Hyp	Ref	Expression
1		ax-17 1526	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	eximdh 1611	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:   → wi 4  ∃wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1882  reximdv2  2576  cgsexg  2773  spc3egv  2830  euind  2925  ssel  3150  reupick  3420  reximdva0m  3439  uniss  3831  eusvnfb  4455  coss1  4783  coss2  4784  dmss  4827  dmcosseq  4899  funssres  5259  imain  5299  brprcneu  5509  fv3  5539  dffo4  5665  dffo5  5666  f1eqcocnv  5792  mapsn  6690  ctssdccl  7110  acfun  7206  ccfunen  7263  cc4f  7268  cc4n  7270  dmaddpq  7378  dmmulpq  7379  recexprlemlol  7625  recexprlemupu  7627  ioom  10261  ctinfom  12429  ctinf  12431  omctfn  12444  nninfdclemp1  12451  ptex  12713  subgintm  13058  txcn  13778