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

Theorem simp2r 942
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 107 . 2  |-  ( ( ps  /\  ch )  ->  ch )
213ad2ant2 937 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  simpl2r  969  simpr2r  975  simp12r  1029  simp22r  1035  simp32r  1041  issod  4084  funprg  4977  fsnunf  5390  f1oiso2  5494  tfrlemibxssdm  5972  ecopovtrn  6234  ecopovtrng  6237  addassnqg  6538  ltsonq  6554  ltanqg  6556  ltmnqg  6557  addassnq0  6618  recexprlem1ssl  6789  mulasssrg  6901  distrsrg  6902  lttrsr  6905  ltsosr  6907  ltasrg  6913  mulextsr1lem  6922  mulextsr1  6923  axmulass  7005  axdistr  7006  dmdcanap  7773  lediv2  7932  ltdiv23  7933  lediv23  7934  expaddzaplem  9463  expaddzap  9464  expmulzap  9466  expdivap  9471  fldivndvdslt  10247
  Copyright terms: Public domain W3C validator