Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  exlimddv GIF version

Theorem exlimddv 1794
 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
StepHypRef Expression
1 exlimddv.1 . 2 (𝜑 → ∃𝑥𝜓)
2 exlimddv.2 . . . 4 ((𝜑𝜓) → 𝜒)
32ex 112 . . 3 (𝜑 → (𝜓𝜒))
43exlimdv 1716 . 2 (𝜑 → (∃𝑥𝜓𝜒))
51, 4mpd 13 1 (𝜑𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101  ∃wex 1397 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie2 1399  ax-17 1435 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  fvmptdv2  5287  tfrlemi14d  5977  tfrexlem  5978  erref  6156  xpdom2  6335  phplem4dom  6354  phplem4on  6359  fidceq  6360  dif1en  6367  fin0  6372  fin0or  6373  genpml  6672  genpmu  6673  ltexprlemm  6755  ltexprlemfl  6764  ltexprlemfu  6766  nn1suc  8008
 Copyright terms: Public domain W3C validator