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  8553  axcclem  8736  enqeq  9213  ltleletr  9577  ixxssixx  11424  muldvds1  13674  dvds2add  13681  dvds2sub  13682  dvdstr  13683  pospropd  15422  csrgbinom  16766  smadiadetglem2  18609  ismbf3d  21264  mbfi1flimlem  21332  colinearalg  23307  2pthon  23652  constr3trllem2  23688  prodmolem2  27591  prodmo  27592  zprod  27593  cgr3permute3  28221  cgr3com  28227  brofs2  28251  areacirclem4  28634  ismrc  29184  iocinico  29734  sigaras  30038  sigarms  30039  leltletr  30320  wlkiswwlkinj  30497  2wlkonotv  30543  usg2spthonot  30554  usg2spthonot0  30555  vdn1frgrav2  30765  vdgn1frgrav2  30766  lincresunit3lem3  31126  lincresunit3  31133  bnj967  32255  bnj1110  32290  paddasslem14  33800  lhpexle1  33975  cdlemk19w  34939
  Copyright terms: Public domain W3C validator