Theorem eximdv 1903

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

Syntax hints:   → wi 4  ∃wex 1515

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1905  reximdv2  2605  cgsexg  2807  spc3egv  2865  euind  2960  ssel  3187  reupick  3457  reximdva0m  3476  uniss  3871  eusvnfb  4501  coss1  4833  coss2  4834  dmss  4877  dmcosseq  4950  funssres  5313  imain  5356  brprcneu  5569  fv3  5599  dffo4  5728  dffo5  5729  f1eqcocnv  5860  mapsn  6777  ctssdccl  7213  acfun  7319  ccfunen  7376  cc4f  7381  cc4n  7383  dmaddpq  7492  dmmulpq  7493  recexprlemlol  7739  recexprlemupu  7741  ioom  10403  ctinfom  12799  ctinf  12801  omctfn  12814  nninfdclemp1  12821  ptex  13096  subgintm  13534  txcn  14747