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  8774  nn1suc  9273  nninfdcex  10621  zsupssdc  10622  seq3f1oleml  10902  zfz1isolem1  11237  eulerth  12955  4sqlem14  13127  4sqlem17  13130  4sqlem18  13131  ennnfonelemim  13259  exmidunben  13261  enctlem  13267  ctiunct  13275  unct  13277  omctfn  13278  omiunct  13279  relelbasov  13359  issubg2m  13990  opprringb  14309  lmff  15226  txcn  15252  suplociccreex  15601  suplociccex  15602  wlkvtxiedg  16452  wlkvtxiedgg  16453  wlkreslem  16485  eulerpathum  16588  3dom  16874  subctctexmid  16886  exmidsbthrlem  16914  sbthom  16918  gfsump1  16980