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

Theorem simp2l 941
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 106 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 937 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
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:  simpl2l  968  simpr2l  974  simp12l  1028  simp22l  1034  simp32l  1040  issod  4084  funprg  4977  fsnunf  5390  f1oiso2  5494  ecopovtrn  6234  ecopovtrng  6237  addassnqg  6538  ltsonq  6554  ltanqg  6556  ltmnqg  6557  addassnq0  6618  recexprlem1ssu  6790  mulasssrg  6901  distrsrg  6902  lttrsr  6905  ltsosr  6907  ltasrg  6913  mulextsr1lem  6922  mulextsr1  6923  axmulass  7005  axdistr  7006  dmdcanap  7773  ltdiv2  7928  lediv2  7932  ltdiv23  7933  lediv23  7934  expaddzaplem  9463  expaddzap  9464  expmulzap  9466  expdivap  9471
  Copyright terms: Public domain W3C validator