Theorem exlimddv 1923

Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
exlimddv.1	⊢ (𝜑 → ∃𝑥𝜓)
exlimddv.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
exlimddv	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimddv

Step	Hyp	Ref	Expression
1		exlimddv.1	. 2 ⊢ (𝜑 → ∃𝑥𝜓)
2		exlimddv.2	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	2	ex 115	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	3	exlimdv 1843	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 13	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104  ∃wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie2 1518  ax-17 1550

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5681  tfrlemi14d  6431  tfrexlem  6432  tfr1onlemres  6447  tfrcllemres  6460  tfrcldm  6461  erref  6652  en2  6925  en2m  6926  xpdom2  6940  dom0  6949  xpen  6956  mapdom1g  6958  phplem4dom  6973  phplem4on  6978  fidceq  6980  dif1en  6990  fin0  6996  fin0or  6997  isinfinf  7008  infm  7015  en2eqpr  7018  fiuni  7094  supelti  7118  djudom  7209  difinfsn  7216  enomnilem  7254  enmkvlem  7277  enwomnilem  7285  exmidfodomrlemim  7324  exmidaclem  7335  cc2lem  7393  cc3  7395  genpml  7645  genpmu  7646  ltexprlemm  7728  ltexprlemfl  7737  ltexprlemfu  7739  suplocsr  7937  axpre-suploc  8030  eqord1  8571  nn1suc  9070  nninfdcex  10397  zsupssdc  10398  seq3f1oleml  10678  zfz1isolem1  11002  eulerth  12625  4sqlem14  12797  4sqlem17  12800  4sqlem18  12801  ennnfonelemim  12865  exmidunben  12867  enctlem  12873  ctiunct  12881  unct  12883  omctfn  12884  omiunct  12885  relelbasov  12964  issubg2m  13595  lmff  14791  txcn  14817  suplociccreex  15166  suplociccex  15167  1dom1el  16061  subctctexmid  16072  exmidsbthrlem  16096  sbthom  16100