Theorem exlimddv 1948

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 1868	. 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  5766  tfrlemi14d  6563  tfrexlem  6564  tfr1onlemres  6579  tfrcllemres  6592  tfrcldm  6593  erref  6786  1dom1el  7059  en2  7064  en2m  7065  xpdom2  7081  dom0  7090  xpen  7097  mapdom1g  7099  phplem4dom  7115  phplem4on  7121  fidceq  7123  dif1en  7135  fin0  7141  fin0or  7142  isinfinf  7153  eqsndc  7162  infm  7163  en2eqpr  7166  fiuni  7264  supelti  7292  djudom  7383  difinfsn  7390  enomnilem  7428  enmkvlem  7451  enwomnilem  7459  exmidfodomrlemim  7503  exmidaclem  7514  cc2lem  7579  cc3  7581  genpml  7831  genpmu  7832  ltexprlemm  7914  ltexprlemfl  7923  ltexprlemfu  7925  suplocsr  8123  axpre-suploc  8216  eqord1  8756  nn1suc  9255  nninfdcex  10596  zsupssdc  10597  seq3f1oleml  10877  zfz1isolem1  11208  eulerth  12926  4sqlem14  13098  4sqlem17  13101  4sqlem18  13102  ennnfonelemim  13167  exmidunben  13169  enctlem  13175  ctiunct  13183  unct  13185  omctfn  13186  omiunct  13187  relelbasov  13267  issubg2m  13898  lmff  15106  txcn  15132  suplociccreex  15481  suplociccex  15482  wlkvtxiedg  16332  wlkvtxiedgg  16333  wlkreslem  16365  eulerpathum  16468  3dom  16754  subctctexmid  16766  exmidsbthrlem  16794  sbthom  16798  gfsump1  16859