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

Theorem 3simpa 940
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 926 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
21simplbi 268 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  3simpb  941  3simpc  942  simp1  943  simp2  944  3adant3  963  3adantl3  1101  3adantr3  1104  opprc  3638  oprcl  3641  opm  4052  funtpg  5051  ftpg  5465  ovig  5748  prltlu  7025  mullocpr  7109  lt2halves  8621  nn0n0n1ge2  8787  ixxssixx  9289  sumtp  10771  dvdsmulcr  10919  dvds2add  10923  dvds2sub  10924  dvdstr  10926  bj-peano4  11507
  Copyright terms: Public domain W3C validator