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

Theorem 3simpa 963
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3simpa  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )

Proof of Theorem 3simpa
StepHypRef Expression
1 df-3an 949 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
21simplbi 272 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  3simpb  964  3simpc  965  simp1  966  simp2  967  3adant3  986  3adantl3  1124  3adantr3  1127  opprc  3696  oprcl  3699  opm  4126  funtpg  5144  ftpg  5572  ovig  5860  prltlu  7263  mullocpr  7347  lt2halves  8923  nn0n0n1ge2  9089  ixxssixx  9653  sumtp  11151  dvdsmulcr  11450  dvds2add  11454  dvds2sub  11455  dvdstr  11457  bj-peano4  13080
  Copyright terms: Public domain W3C validator