Theorem exlimddv 1954

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  fvmptdv2  5798  tfrlemi14d  6609  tfrexlem  6610  tfr1onlemres  6625  tfrcllemres  6638  tfrcldm  6639  erref  6832  1dom1el  7113  en2  7118  en2m  7119  xpdom2  7135  dom0  7144  xpen  7151  mapdom1g  7153  phplem4dom  7169  phplem4on  7175  fidceq  7177  dif1en  7189  fin0  7195  fin0or  7196  isinfinf  7207  eqsndc  7216  infm  7217  en2eqpr  7220  funisfsuppdc  7299  fiuni  7318  supelti  7349  djudom  7440  difinfsn  7447  enomnilem  7485  enmkvlem  7508  enwomnilem  7516  exmidfodomrlemim  7560  exmidaclem  7571  cc2lem  7639  cc3  7641  genpml  7891  genpmu  7892  ltexprlemm  7974  ltexprlemfl  7983  ltexprlemfu  7985  suplocsr  8183  axpre-suploc  8276  eqord1  8819  nn1suc  9333  nninfdcex  10689  zsupssdc  10690  seq3f1oleml  10974  zfz1isolem1  11314  eulerth  13040  4sqlem14  13212  4sqlem17  13215  4sqlem18  13216  ennnfonelemim  13373  exmidunben  13375  enctlem  13381  ctiunct  13389  unct  13391  omctfn  13392  omiunct  13393  relelbasov  13474  issubg2m  14051  gsump1  14247  gsumf1ofi  14250  gsummhmfi  14264  gsumressfi  14267  opprringb  14495  psrbagmax  15190  psrbagfsuppub  15192  mplsubgfilemcl  15246  mplsubgfileminv  15247  lmff  15508  txcn  15534  suplociccreex  15883  suplociccex  15884  wlkvtxiedg  16824  wlkvtxiedgg  16825  wlkreslem  16857  eulerpathum  16960  3dom  17256  subctctexmid  17268  exmidsbthrlem  17306  sbthom  17310