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

Theorem 3simpb 994
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 982 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ch  /\ 
ps ) )
2 3simpa 993 . 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 369    /\ w3a 973
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 371  df-3an 975
This theorem is referenced by:  3adant2  1015  3adantl2  1153  3adantr2  1156  cfcof  8650  axcclem  8833  enqeq  9308  ltleletr  9673  ixxssixx  11539  muldvds1  13862  dvds2add  13869  dvds2sub  13870  dvdstr  13871  pospropd  15614  csrgbinom  16982  smadiadetglem2  18938  ismbf3d  21793  mbfi1flimlem  21861  colinearalg  23886  2pthon  24277  constr3trllem2  24324  wlkiswwlkinj  24391  2wlkonotv  24550  usg2spthonot  24561  usg2spthonot0  24562  vdn1frgrav2  24699  vdgn1frgrav2  24700  prodmolem2  28641  prodmo  28642  zprod  28643  cgr3permute3  29271  cgr3com  29277  brofs2  29301  areacirclem4  29685  ismrc  30235  iocinico  30784  itgspltprt  31297  fourierdlem113  31520  sigaras  31539  sigarms  31540  leltletr  31787  lincresunit3lem3  32148  lincresunit3  32155  bnj967  33082  bnj1110  33117  paddasslem14  34629  lhpexle1  34804  cdlemk19w  35768
  Copyright terms: Public domain W3C validator