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

Theorem 3simpa 978
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 964 . 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 962
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 964
This theorem is referenced by:  3simpb  979  3simpc  980  simp1  981  simp2  982  3adant3  1001  3adantl3  1139  3adantr3  1142  opprc  3726  oprcl  3729  opm  4156  funtpg  5174  ftpg  5604  ovig  5892  prltlu  7302  mullocpr  7386  lt2halves  8962  nn0n0n1ge2  9128  ixxssixx  9692  sumtp  11190  dvdsmulcr  11529  dvds2add  11533  dvds2sub  11534  dvdstr  11536  bj-peano4  13206
  Copyright terms: Public domain W3C validator