Theorem eximdv 1760

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

Syntax hints:   → wi 4  ∃wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2eximdv  1762  reximdv2  2418  cgsexg  2589  spc3egv  2644  euind  2728  ssel  2939  reupick  3221  reximdva0m  3236  uniss  3601  eusvnfb  4186  coss1  4491  coss2  4492  dmss  4534  dmcosseq  4603  funssres  4942  imain  4981  brprcneu  5171  fv3  5197  dffo4  5315  dffo5  5316  f1eqcocnv  5431  dmaddpq  6477  dmmulpq  6478  recexprlemlol  6724  recexprlemupu  6726