Theorem eximdv 1928

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 1575	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	eximdh 1660	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:   → wi 4  ∃wex 1541

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1930  reximdv2  2632  cgsexg  2839  spc3egv  2899  euind  2994  ssel  3222  reupick  3493  reximdva0m  3512  uniss  3919  eusvnfb  4557  coss1  4891  coss2  4892  ssrelrn  4928  dmss  4936  dmcosseq  5010  funssres  5376  imain  5419  brprcneu  5641  fv3  5671  dffo4  5803  dffo5  5804  f1eqcocnv  5942  mapsn  6902  en2m  7042  ctssdccl  7353  acfun  7465  ccfunen  7526  cc4f  7531  cc4n  7533  dmaddpq  7642  dmmulpq  7643  recexprlemlol  7889  recexprlemupu  7891  ioom  10566  ctinfom  13112  ctinf  13114  omctfn  13127  nninfdclemp1  13134  ptex  13410  subgintm  13848  txcn  15069