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

Syntax hints:   → wi 4  ∃wex 1540

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1930  reximdv2  2631  cgsexg  2838  spc3egv  2898  euind  2993  ssel  3221  reupick  3491  reximdva0m  3510  uniss  3914  eusvnfb  4551  coss1  4885  coss2  4886  ssrelrn  4922  dmss  4930  dmcosseq  5004  funssres  5369  imain  5412  brprcneu  5632  fv3  5662  dffo4  5795  dffo5  5796  f1eqcocnv  5932  mapsn  6859  en2m  6999  ctssdccl  7310  acfun  7422  ccfunen  7483  cc4f  7488  cc4n  7490  dmaddpq  7599  dmmulpq  7600  recexprlemlol  7846  recexprlemupu  7848  ioom  10521  ctinfom  13054  ctinf  13056  omctfn  13069  nninfdclemp1  13076  ptex  13352  subgintm  13790  txcn  15005