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

Theorem exlimddv 1794
Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
exlimddv.1  |-  ( ph  ->  E. x ps )
exlimddv.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
exlimddv  |-  ( ph  ->  ch )
Distinct variable groups:    ch, x    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem exlimddv
StepHypRef Expression
1 exlimddv.1 . 2  |-  ( ph  ->  E. x ps )
2 exlimddv.2 . . . 4  |-  ( (
ph  /\  ps )  ->  ch )
32ex 112 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
43exlimdv 1716 . 2  |-  ( ph  ->  ( E. x ps 
->  ch ) )
51, 4mpd 13 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101   E.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  5288  tfrlemi14d  5978  tfrexlem  5979  erref  6157  xpdom2  6336  phplem4dom  6355  phplem4on  6360  fidceq  6361  dif1en  6368  fin0  6373  fin0or  6374  genpml  6673  genpmu  6674  ltexprlemm  6756  ltexprlemfl  6765  ltexprlemfu  6767  nn1suc  8009
  Copyright terms: Public domain W3C validator