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

Theorem simp2l 970
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 108 . 2  |-  ( ( ps  /\  ch )  ->  ps )
213ad2ant2 966 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 925
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 927
This theorem is referenced by:  simpl2l  997  simpr2l  1003  simp12l  1057  simp22l  1063  simp32l  1069  issod  4157  funprg  5079  fsnunf  5513  f1oiso2  5622  ecopovtrn  6405  ecopovtrng  6408  addassnqg  7004  ltsonq  7020  ltanqg  7022  ltmnqg  7023  addassnq0  7084  recexprlem1ssu  7256  mulasssrg  7367  distrsrg  7368  lttrsr  7371  ltsosr  7373  ltasrg  7379  mulextsr1lem  7388  mulextsr1  7389  axmulass  7471  axdistr  7472  dmdcanap  8252  ltdiv2  8411  lediv2  8415  ltdiv23  8416  lediv23  8417  expaddzaplem  10061  expaddzap  10062  expmulzap  10064  expdivap  10069  leisorel  10305  fsumsplitsnun  10876  prmexpb  11471
  Copyright terms: Public domain W3C validator