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

Theorem 3simpb 955
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 945 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ch  /\ 
ps ) )
2 3simpa 954 . 2  |-  ( (
ph  /\  ch  /\  ps )  ->  ( ph  /\  ch ) )
31, 2sylbi 188 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3adant2  976  3adantl2  1114  3adantr2  1117  cfcof  8110  axcclem  8293  enqeq  8767  ixxssixx  10886  muldvds1  12829  dvds2add  12836  dvds2sub  12837  dvdstr  12838  pospropd  14516  ismbf3d  19499  mbfi1flimlem  19567  2pthon  21555  constr3trllem2  21591  prodmolem2  25214  prodmo  25215  zprod  25216  colinearalg  25753  cgr3permute3  25885  cgr3com  25891  brofs2  25915  areacirclem5  26185  ismrc  26645  sigaras  27712  sigarms  27713  2wlkonotv  28074  usg2spthonot  28085  usg2spthonot0  28086  vdn1frgrav2  28130  vdgn1frgrav2  28131  bnj967  29022  bnj1110  29057  paddasslem14  30315  lhpexle1  30490  cdlemk19w  31454
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator