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

Theorem exlimddv 1821
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 113 . . 3 (𝜑 → (𝜓𝜒))
43exlimdv 1742 . 2 (𝜑 → (∃𝑥𝜓𝜒))
51, 4mpd 13 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie2 1424  ax-17 1460
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  fvmptdv2  5337  tfrlemi14d  6030  tfrexlem  6031  tfr1onlemres  6046  tfrcllemres  6059  tfrcldm  6060  erref  6242  xpdom2  6477  dom0  6484  xpen  6491  mapdom1g  6493  phplem4dom  6508  phplem4on  6513  fidceq  6515  dif1en  6525  fin0  6531  fin0or  6532  isinfinf  6543  infm  6547  en2eqpr  6550  supelti  6604  djudom  6694  enomnilem  6699  exmidfodomrlemim  6730  genpml  6979  genpmu  6980  ltexprlemm  7062  ltexprlemfl  7071  ltexprlemfu  7073  nn1suc  8335
  Copyright terms: Public domain W3C validator