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

Theorem exlimddv 1833
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 114 . . 3 (𝜑 → (𝜓𝜒))
43exlimdv 1754 . 2 (𝜑 → (∃𝑥𝜓𝜒))
51, 4mpd 13 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wex 1433
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie2 1435  ax-17 1471
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  fvmptdv2  5428  tfrlemi14d  6136  tfrexlem  6137  tfr1onlemres  6152  tfrcllemres  6165  tfrcldm  6166  erref  6352  xpdom2  6627  dom0  6634  xpen  6641  mapdom1g  6643  phplem4dom  6658  phplem4on  6663  fidceq  6665  dif1en  6675  fin0  6681  fin0or  6682  isinfinf  6693  infm  6700  en2eqpr  6703  supelti  6777  djudom  6863  enomnilem  6881  exmidfodomrlemim  6924  genpml  7173  genpmu  7174  ltexprlemm  7256  ltexprlemfl  7265  ltexprlemfu  7267  eqord1  8058  nn1suc  8539  seq3f1oleml  10053  zfz1isolem1  10360  lmff  12100  exmidsbthrlem  12617
  Copyright terms: Public domain W3C validator