Theorem exlimddv 1945

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5726  tfrlemi14d  6485  tfrexlem  6486  tfr1onlemres  6501  tfrcllemres  6514  tfrcldm  6515  erref  6708  en2  6981  en2m  6982  xpdom2  6998  dom0  7007  xpen  7014  mapdom1g  7016  phplem4dom  7031  phplem4on  7037  fidceq  7039  dif1en  7049  fin0  7055  fin0or  7056  isinfinf  7067  infm  7074  en2eqpr  7077  fiuni  7153  supelti  7177  djudom  7268  difinfsn  7275  enomnilem  7313  enmkvlem  7336  enwomnilem  7344  exmidfodomrlemim  7387  exmidaclem  7398  cc2lem  7460  cc3  7462  genpml  7712  genpmu  7713  ltexprlemm  7795  ltexprlemfl  7804  ltexprlemfu  7806  suplocsr  8004  axpre-suploc  8097  eqord1  8638  nn1suc  9137  nninfdcex  10465  zsupssdc  10466  seq3f1oleml  10746  zfz1isolem1  11070  eulerth  12763  4sqlem14  12935  4sqlem17  12938  4sqlem18  12939  ennnfonelemim  13003  exmidunben  13005  enctlem  13011  ctiunct  13019  unct  13021  omctfn  13022  omiunct  13023  relelbasov  13103  issubg2m  13734  lmff  14931  txcn  14957  suplociccreex  15306  suplociccex  15307  wlkvtxiedg  16066  wlkvtxiedgg  16067  wlkreslem  16097  1dom1el  16378  3dom  16381  subctctexmid  16395  exmidsbthrlem  16420  sbthom  16424