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  5931  mapsn  6858  en2m  6998  ctssdccl  7309  acfun  7421  ccfunen  7482  cc4f  7487  cc4n  7489  dmaddpq  7598  dmmulpq  7599  recexprlemlol  7845  recexprlemupu  7847  ioom  10519  ctinfom  13048  ctinf  13050  omctfn  13063  nninfdclemp1  13070  ptex  13346  subgintm  13784  txcn  14998