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  7900  axcclem  8083  enqeq  8558  ixxssixx  10670  muldvds1  12553  dvds2add  12560  dvds2sub  12561  dvdstr  12562  pospropd  14238  ismbf3d  19009  mbfi1flimlem  19077  colinearalg  24538  cgr3permute3  24670  cgr3com  24676  brofs2  24700  areacirclem5  24929  cmpmon  25815  icmpmon  25816  ismrc  26776  fmuldfeq  27713  stoweidlem31  27780  stoweidlem34  27783  stoweidlem44  27793  sigaras  27845  sigarms  27846  bnj967  28977  bnj1110  29012  paddasslem14  30022  lhpexle1  30197  cdlemk19w  31161
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