Theorem exlimddv 1947

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 1867	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 13	1 ⊢ (𝜑 → 𝜒)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5745  tfrlemi14d  6542  tfrexlem  6543  tfr1onlemres  6558  tfrcllemres  6571  tfrcldm  6572  erref  6765  1dom1el  7036  en2  7041  en2m  7042  xpdom2  7058  dom0  7067  xpen  7074  mapdom1g  7076  phplem4dom  7091  phplem4on  7097  fidceq  7099  dif1en  7111  fin0  7117  fin0or  7118  isinfinf  7129  eqsndc  7138  infm  7139  en2eqpr  7142  fiuni  7220  supelti  7244  djudom  7335  difinfsn  7342  enomnilem  7380  enmkvlem  7403  enwomnilem  7411  exmidfodomrlemim  7455  exmidaclem  7466  cc2lem  7528  cc3  7530  genpml  7780  genpmu  7781  ltexprlemm  7863  ltexprlemfl  7872  ltexprlemfu  7874  suplocsr  8072  axpre-suploc  8165  eqord1  8706  nn1suc  9205  nninfdcex  10541  zsupssdc  10542  seq3f1oleml  10822  zfz1isolem1  11148  eulerth  12866  4sqlem14  13038  4sqlem17  13041  4sqlem18  13042  ennnfonelemim  13106  exmidunben  13108  enctlem  13114  ctiunct  13122  unct  13124  omctfn  13125  omiunct  13126  relelbasov  13206  issubg2m  13837  lmff  15040  txcn  15066  suplociccreex  15415  suplociccex  15416  wlkvtxiedg  16266  wlkvtxiedgg  16267  wlkreslem  16299  eulerpathum  16402  3dom  16688  subctctexmid  16702  exmidsbthrlem  16730  sbthom  16734  gfsump1  16795