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

Theorem simp2l 969
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp2l  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 107 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 965 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  simpl2l  996  simpr2l  1002  simp12l  1056  simp22l  1062  simp32l  1068  issod  4146  funprg  5064  fsnunf  5497  f1oiso2  5606  ecopovtrn  6389  ecopovtrng  6392  addassnqg  6941  ltsonq  6957  ltanqg  6959  ltmnqg  6960  addassnq0  7021  recexprlem1ssu  7193  mulasssrg  7304  distrsrg  7305  lttrsr  7308  ltsosr  7310  ltasrg  7316  mulextsr1lem  7325  mulextsr1  7326  axmulass  7408  axdistr  7409  dmdcanap  8189  ltdiv2  8348  lediv2  8352  ltdiv23  8353  lediv23  8354  expaddzaplem  9998  expaddzap  9999  expmulzap  10001  expdivap  10006  leisorel  10242  fsumsplitsnun  10813  prmexpb  11408
  Copyright terms: Public domain W3C validator