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

Theorem 3simpb 995
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 983 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ch  /\ 
ps ) )
2 3simpa 994 . 2  |-  ( (
ph  /\  ch  /\  ps )  ->  ( ph  /\  ch ) )
31, 2sylbi 195 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 976
This theorem is referenced by:  3adant2  1016  3adantl2  1154  3adantr2  1157  cfcof  8686  axcclem  8869  enqeq  9342  ltleletr  9708  ixxssixx  11596  prodmolem2  13894  prodmo  13895  zprod  13896  muldvds1  14217  dvds2add  14224  dvds2sub  14225  dvdstr  14227  initoeu2lem2  15618  pospropd  16088  csrgbinom  17517  smadiadetglem2  19466  ismbf3d  22353  mbfi1flimlem  22421  colinearalg  24630  2pthon  25021  constr3trllem2  25068  wlkiswwlkinj  25135  2wlkonotv  25294  usg2spthonot  25305  usg2spthonot0  25306  vdn1frgrav2  25442  vdgn1frgrav2  25443  bnj967  29330  bnj1110  29365  cgr3permute3  30385  cgr3com  30391  brofs2  30415  areacirclem4  31481  paddasslem14  32850  lhpexle1  33025  cdlemk19w  33991  ismrc  34995  iocinico  35543  fourierdlem113  37370  sigaras  37440  sigarms  37441  leltletr  37665  lincresunit3lem3  38586  lincresunit3  38593
  Copyright terms: Public domain W3C validator