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

Theorem 3simpb 986
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 974 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ch  /\ 
ps ) )
2 3simpa 985 . 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 965
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 967
This theorem is referenced by:  3adant2  1007  3adantl2  1145  3adantr2  1148  cfcof  8435  axcclem  8618  enqeq  9095  ltleletr  9459  ixxssixx  11306  muldvds1  13549  dvds2add  13556  dvds2sub  13557  dvdstr  13558  pospropd  15296  csrgbinom  16634  smadiadetglem2  18458  ismbf3d  21112  mbfi1flimlem  21180  colinearalg  23128  2pthon  23473  constr3trllem2  23509  prodmolem2  27421  prodmo  27422  zprod  27423  cgr3permute3  28051  cgr3com  28057  brofs2  28081  areacirclem4  28461  ismrc  29011  iocinico  29561  sigaras  29865  sigarms  29866  leltletr  30147  wlkiswwlkinj  30324  2wlkonotv  30370  usg2spthonot  30381  usg2spthonot0  30382  vdn1frgrav2  30592  vdgn1frgrav2  30593  lincresunit3lem3  30942  lincresunit3  30949  bnj967  31870  bnj1110  31905  paddasslem14  33394  lhpexle1  33569  cdlemk19w  34533
  Copyright terms: Public domain W3C validator