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 ⊢ (𝜑 → 𝜒)

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

This theorem was proved from 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 theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5792  tfrlemi14d  6598  tfrexlem  6599  tfr1onlemres  6614  tfrcllemres  6627  tfrcldm  6628  erref  6821  1dom1el  7101  en2  7106  en2m  7107  xpdom2  7123  dom0  7132  xpen  7139  mapdom1g  7141  phplem4dom  7157  phplem4on  7163  fidceq  7165  dif1en  7177  fin0  7183  fin0or  7184  isinfinf  7195  eqsndc  7204  infm  7205  en2eqpr  7208  fiuni  7306  supelti  7336  djudom  7427  difinfsn  7434  enomnilem  7472  enmkvlem  7495  enwomnilem  7503  exmidfodomrlemim  7547  exmidaclem  7558  cc2lem  7626  cc3  7628  genpml  7878  genpmu  7879  ltexprlemm  7961  ltexprlemfl  7970  ltexprlemfu  7972  suplocsr  8170  axpre-suploc  8263  eqord1  8805  nn1suc  9306  nninfdcex  10655  zsupssdc  10656  seq3f1oleml  10936  zfz1isolem1  11275  eulerth  12994  4sqlem14  13166  4sqlem17  13169  4sqlem18  13170  ennnfonelemim  13298  exmidunben  13300  enctlem  13306  ctiunct  13314  unct  13316  omctfn  13317  omiunct  13318  relelbasov  13399  issubg2m  13975  gsump1  14140  gsumf1ofi  14143  gsummhmfi  14147  gsumressfi  14150  opprringb  14369  lmff  15333  txcn  15359  suplociccreex  15708  suplociccex  15709  wlkvtxiedg  16569  wlkvtxiedgg  16570  wlkreslem  16602  eulerpathum  16705  3dom  17001  subctctexmid  17013  exmidsbthrlem  17041  sbthom  17045