Theorem exlimddv 1950

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  5772  tfrlemi14d  6577  tfrexlem  6578  tfr1onlemres  6593  tfrcllemres  6606  tfrcldm  6607  erref  6800  1dom1el  7073  en2  7078  en2m  7079  xpdom2  7095  dom0  7104  xpen  7111  mapdom1g  7113  phplem4dom  7129  phplem4on  7135  fidceq  7137  dif1en  7149  fin0  7155  fin0or  7156  isinfinf  7167  eqsndc  7176  infm  7177  en2eqpr  7180  fiuni  7278  supelti  7306  djudom  7397  difinfsn  7404  enomnilem  7442  enmkvlem  7465  enwomnilem  7473  exmidfodomrlemim  7517  exmidaclem  7528  cc2lem  7596  cc3  7598  genpml  7848  genpmu  7849  ltexprlemm  7931  ltexprlemfl  7940  ltexprlemfu  7942  suplocsr  8140  axpre-suploc  8233  eqord1  8775  nn1suc  9276  nninfdcex  10624  zsupssdc  10625  seq3f1oleml  10905  zfz1isolem1  11240  eulerth  12959  4sqlem14  13131  4sqlem17  13134  4sqlem18  13135  ennnfonelemim  13263  exmidunben  13265  enctlem  13271  ctiunct  13279  unct  13281  omctfn  13282  omiunct  13283  relelbasov  13363  issubg2m  13946  gfsump1  14112  opprringb  14328  lmff  15244  txcn  15270  suplociccreex  15619  suplociccex  15620  wlkvtxiedg  16470  wlkvtxiedgg  16471  wlkreslem  16503  eulerpathum  16606  3dom  16902  subctctexmid  16914  exmidsbthrlem  16942  sbthom  16946