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  8705  nn1suc  9204  nninfdcex  10543  zsupssdc  10544  seq3f1oleml  10824  zfz1isolem1  11150  eulerth  12868  4sqlem14  13040  4sqlem17  13043  4sqlem18  13044  ennnfonelemim  13108  exmidunben  13110  enctlem  13116  ctiunct  13124  unct  13126  omctfn  13127  omiunct  13128  relelbasov  13208  issubg2m  13839  lmff  15043  txcn  15069  suplociccreex  15418  suplociccex  15419  wlkvtxiedg  16269  wlkvtxiedgg  16270  wlkreslem  16302  eulerpathum  16405  3dom  16691  subctctexmid  16705  exmidsbthrlem  16733  sbthom  16737  gfsump1  16798