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

Theorem 3simpb 994
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3simpb

Proof of Theorem 3simpb
StepHypRef Expression
1 3ancomb 982 . 2
2 3simpa 993 . 2
31, 2sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  3adant2  1015  3adantl2  1153  3adantr2  1156  cfcof  8675  axcclem  8858  enqeq  9333  ltleletr  9698  ixxssixx  11572  prodmolem2  13742  prodmo  13743  zprod  13744  muldvds1  14008  dvds2add  14015  dvds2sub  14016  dvdstr  14018  pospropd  15764  csrgbinom  17197  smadiadetglem2  19174  ismbf3d  22061  mbfi1flimlem  22129  colinearalg  24213  2pthon  24604  constr3trllem2  24651  wlkiswwlkinj  24718  2wlkonotv  24877  usg2spthonot  24888  usg2spthonot0  24889  vdn1frgrav2  25025  vdgn1frgrav2  25026  cgr3permute3  29697  cgr3com  29703  brofs2  29727  areacirclem4  30110  ismrc  30633  iocinico  31179  fourierdlem113  32002  sigaras  32072  sigarms  32073  leltletr  32318  initoeu2lem2  32621  lincresunit3lem3  33075  lincresunit3  33082  bnj967  34003  bnj1110  34038  paddasslem14  35557  lhpexle1  35732  cdlemk19w  36698
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
  Copyright terms: Public domain W3C validator