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  5795  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemres  6620  tfrcllemres  6633  tfrcldm  6634  erref  6827  1dom1el  7107  en2  7112  en2m  7113  xpdom2  7129  dom0  7138  xpen  7145  mapdom1g  7147  phplem4dom  7163  phplem4on  7169  fidceq  7171  dif1en  7183  fin0  7189  fin0or  7190  isinfinf  7201  eqsndc  7210  infm  7211  en2eqpr  7214  fiuni  7312  supelti  7342  djudom  7433  difinfsn  7440  enomnilem  7478  enmkvlem  7501  enwomnilem  7509  exmidfodomrlemim  7553  exmidaclem  7564  cc2lem  7632  cc3  7634  genpml  7884  genpmu  7885  ltexprlemm  7967  ltexprlemfl  7976  ltexprlemfu  7978  suplocsr  8176  axpre-suploc  8269  eqord1  8811  nn1suc  9324  nninfdcex  10674  zsupssdc  10675  seq3f1oleml  10955  zfz1isolem1  11294  eulerth  13013  4sqlem14  13185  4sqlem17  13188  4sqlem18  13189  ennnfonelemim  13317  exmidunben  13319  enctlem  13325  ctiunct  13333  unct  13335  omctfn  13336  omiunct  13337  relelbasov  13418  issubg2m  13994  gsump1  14159  gsumf1ofi  14162  gsummhmfi  14166  gsumressfi  14169  opprringb  14388  lmff  15352  txcn  15378  suplociccreex  15727  suplociccex  15728  wlkvtxiedg  16598  wlkvtxiedgg  16599  wlkreslem  16631  eulerpathum  16734  3dom  17030  subctctexmid  17042  exmidsbthrlem  17079  sbthom  17083