Theorem eximdv 1904

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

Syntax hints:   → wi 4  ∃wex 1516

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1906  reximdv2  2607  cgsexg  2812  spc3egv  2872  euind  2967  ssel  3195  reupick  3465  reximdva0m  3484  uniss  3885  eusvnfb  4519  coss1  4851  coss2  4852  ssrelrn  4888  dmss  4896  dmcosseq  4969  funssres  5332  imain  5375  brprcneu  5592  fv3  5622  dffo4  5751  dffo5  5752  f1eqcocnv  5883  mapsn  6800  en2m  6937  ctssdccl  7239  acfun  7350  ccfunen  7411  cc4f  7416  cc4n  7418  dmaddpq  7527  dmmulpq  7528  recexprlemlol  7774  recexprlemupu  7776  ioom  10440  ctinfom  12914  ctinf  12916  omctfn  12929  nninfdclemp1  12936  ptex  13211  subgintm  13649  txcn  14862