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

Theorem 3simpa 936
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 922 . 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 920
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 922
This theorem is referenced by:  3simpb  937  3simpc  938  simp1  939  simp2  940  3adant3  959  3adantl3  1097  3adantr3  1100  opprc  3599  oprcl  3602  opm  3997  funtpg  4981  ftpg  5379  ovig  5653  prltlu  6739  mullocpr  6823  lt2halves  8333  nn0n0n1ge2  8499  ixxssixx  9001  dvdsmulcr  10370  dvds2add  10374  dvds2sub  10375  dvdstr  10377  bj-peano4  10908
  Copyright terms: Public domain W3C validator