Theorem exlimddv 1913

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie2 1508  ax-17 1540

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5654  tfrlemi14d  6400  tfrexlem  6401  tfr1onlemres  6416  tfrcllemres  6429  tfrcldm  6430  erref  6621  xpdom2  6899  dom0  6908  xpen  6915  mapdom1g  6917  phplem4dom  6932  phplem4on  6937  fidceq  6939  dif1en  6949  fin0  6955  fin0or  6956  isinfinf  6967  infm  6974  en2eqpr  6977  fiuni  7053  supelti  7077  djudom  7168  difinfsn  7175  enomnilem  7213  enmkvlem  7236  enwomnilem  7244  exmidfodomrlemim  7282  exmidaclem  7293  cc2lem  7351  cc3  7353  genpml  7603  genpmu  7604  ltexprlemm  7686  ltexprlemfl  7695  ltexprlemfu  7697  suplocsr  7895  axpre-suploc  7988  eqord1  8529  nn1suc  9028  nninfdcex  10346  zsupssdc  10347  seq3f1oleml  10627  zfz1isolem1  10951  eulerth  12428  4sqlem14  12600  4sqlem17  12603  4sqlem18  12604  ennnfonelemim  12668  exmidunben  12670  enctlem  12676  ctiunct  12684  unct  12686  omctfn  12687  omiunct  12688  relelbasov  12767  issubg2m  13397  lmff  14593  txcn  14619  suplociccreex  14968  suplociccex  14969  1dom1el  15745  subctctexmid  15755  exmidsbthrlem  15779  sbthom  15783