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

Theorem simp2l 1007
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 1003 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  simpl2l  1034  simpr2l  1040  simp12l  1094  simp22l  1100  simp32l  1106  issod  4241  funprg  5173  fsnunf  5620  f1oiso2  5728  ecopovtrn  6526  ecopovtrng  6529  addassnqg  7197  ltsonq  7213  ltanqg  7215  ltmnqg  7216  addassnq0  7277  recexprlem1ssu  7449  mulasssrg  7573  distrsrg  7574  lttrsr  7577  ltsosr  7579  ltasrg  7585  mulextsr1lem  7595  mulextsr1  7596  axmulass  7688  axdistr  7689  dmdcanap  8489  ltdiv2  8652  lediv2  8656  ltdiv23  8657  lediv23  8658  xaddass  9659  xaddass2  9660  xlt2add  9670  expaddzaplem  10343  expaddzap  10344  expmulzap  10346  expdivap  10351  leisorel  10587  bdtrilem  11017  bdtri  11018  xrbdtri  11052  fsumsplitsnun  11195  prmexpb  11836  cnptoprest  12418  ssblps  12604  ssbl  12605  tgqioo  12726
  Copyright terms: Public domain W3C validator