MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3simpb Structured version   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  8154  axcclem  8337  enqeq  8811  ixxssixx  10930  muldvds1  12874  dvds2add  12881  dvds2sub  12882  dvdstr  12883  pospropd  14561  ismbf3d  19546  mbfi1flimlem  19614  2pthon  21602  constr3trllem2  21638  prodmolem2  25261  prodmo  25262  zprod  25263  colinearalg  25849  cgr3permute3  25981  cgr3com  25987  brofs2  26011  areacirclem4  26295  ismrc  26755  sigaras  27821  sigarms  27822  2wlkonotv  28344  usg2spthonot  28355  usg2spthonot0  28356  vdn1frgrav2  28416  vdgn1frgrav2  28417  bnj967  29316  bnj1110  29351  paddasslem14  30630  lhpexle1  30805  cdlemk19w  31769
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