Theorem eximdv 1832

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

Syntax hints:   → wi 4  ∃wex 1449

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximdv  1834  reximdv2  2503  cgsexg  2690  spc3egv  2746  euind  2838  ssel  3055  reupick  3324  reximdva0m  3342  uniss  3721  eusvnfb  4333  coss1  4652  coss2  4653  dmss  4696  dmcosseq  4766  funssres  5121  imain  5161  brprcneu  5366  fv3  5396  dffo4  5520  dffo5  5521  f1eqcocnv  5644  mapsn  6536  ctssdccl  6946  acfun  7008  dmaddpq  7129  dmmulpq  7130  recexprlemlol  7376  recexprlemupu  7378  ioom  9925  ctinfom  11780  ctinf  11782  txcn  12280