Theorem exlimddv 1886

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

Syntax hints:   → wi 4   ∧ wa 103  ∃wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie2 1482  ax-17 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  fvmptdv2  5574  tfrlemi14d  6297  tfrexlem  6298  tfr1onlemres  6313  tfrcllemres  6326  tfrcldm  6327  erref  6517  xpdom2  6793  dom0  6800  xpen  6807  mapdom1g  6809  phplem4dom  6824  phplem4on  6829  fidceq  6831  dif1en  6841  fin0  6847  fin0or  6848  isinfinf  6859  infm  6866  en2eqpr  6869  fiuni  6939  supelti  6963  djudom  7054  difinfsn  7061  enomnilem  7098  enmkvlem  7121  enwomnilem  7129  exmidfodomrlemim  7153  exmidaclem  7160  cc2lem  7203  cc3  7205  genpml  7454  genpmu  7455  ltexprlemm  7537  ltexprlemfl  7546  ltexprlemfu  7548  suplocsr  7746  axpre-suploc  7839  eqord1  8377  nn1suc  8872  seq3f1oleml  10434  zfz1isolem1  10749  nninfdcex  11882  zsupssdc  11883  eulerth  12161  ennnfonelemim  12353  exmidunben  12355  enctlem  12361  ctiunct  12369  unct  12371  omctfn  12372  omiunct  12373  lmff  12849  txcn  12875  suplociccreex  13202  suplociccex  13203  subctctexmid  13841  exmidsbthrlem  13861  sbthom  13865