MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3simpb Unicode version

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

Proof of Theorem 3simpb
StepHypRef Expression
1 3ancomb 943 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ch  /\ 
ps ) )
2 3simpa 952 . 2  |-  ( (
ph  /\  ch  /\  ps )  ->  ( ph  /\  ch ) )
31, 2sylbi 187 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3adant2  974  3adantl2  1112  3adantr2  1115  cfcof  7916  axcclem  8099  enqeq  8574  ixxssixx  10686  muldvds1  12569  dvds2add  12576  dvds2sub  12577  dvdstr  12578  pospropd  14254  ismbf3d  19025  mbfi1flimlem  19093  zprod  24160  colinearalg  24610  cgr3permute3  24742  cgr3com  24748  brofs2  24772  areacirclem5  25032  cmpmon  25918  icmpmon  25919  ismrc  26879  fmuldfeq  27816  stoweidlem31  27883  stoweidlem34  27886  stoweidlem44  27896  sigaras  27948  sigarms  27949  bnj967  29293  bnj1110  29328  paddasslem14  30644  lhpexle1  30819  cdlemk19w  31783
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator