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

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

Proof of Theorem simp2r
StepHypRef Expression
1 simpr 108 . 2  |-  ( ( ps  /\  ch )  ->  ch )
213ad2ant2 965 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ch )
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:  simpl2r  997  simpr2r  1003  simp12r  1057  simp22r  1063  simp32r  1069  issod  4137  funprg  5050  fsnunf  5480  f1oiso2  5588  tfrlemibxssdm  6074  ecopovtrn  6369  ecopovtrng  6372  addassnqg  6920  ltsonq  6936  ltanqg  6938  ltmnqg  6939  addassnq0  7000  recexprlem1ssl  7171  mulasssrg  7283  distrsrg  7284  lttrsr  7287  ltsosr  7289  ltasrg  7295  mulextsr1lem  7304  mulextsr1  7305  axmulass  7387  axdistr  7388  dmdcanap  8163  lediv2  8324  ltdiv23  8325  lediv23  8326  expaddzaplem  9963  expaddzap  9964  expmulzap  9966  expdivap  9971  leisorel  10207  fldivndvdslt  11017  prmexpb  11212
  Copyright terms: Public domain W3C validator