Theorem eximdv 1860

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

Syntax hints:   → wi 4  ∃wex 1472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximdv  1862  reximdv2  2556  cgsexg  2747  spc3egv  2804  euind  2899  ssel  3122  reupick  3391  reximdva0m  3409  uniss  3793  eusvnfb  4413  coss1  4740  coss2  4741  dmss  4784  dmcosseq  4856  funssres  5211  imain  5251  brprcneu  5460  fv3  5490  dffo4  5614  dffo5  5615  f1eqcocnv  5738  mapsn  6632  ctssdccl  7049  acfun  7136  ccfunen  7178  cc4f  7183  cc4n  7185  dmaddpq  7293  dmmulpq  7294  recexprlemlol  7540  recexprlemupu  7542  ioom  10153  ctinfom  12140  ctinf  12142  omctfn  12155  txcn  12646