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

Theorem 3simpc 954
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Assertion
Ref Expression
3simpc  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  ch ) )

Proof of Theorem 3simpc
StepHypRef Expression
1 3anrot 939 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
2 3simpa 952 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  ( ps  /\ 
ch ) )
31, 2sylbi 187 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simp3  957  3adant1  973  3adantl1  1111  3adantr1  1114  eupickb  2221  find  4697  riotasv2s  6367  tz7.49c  6474  eqsup  7223  mulcanenq  8600  elnpi  8628  divcan2  9448  diveq0  9450  divrec  9456  divcan3  9464  eliooord  10726  fzrev3  10865  sqdiv  11185  sqrmo  11753  muldvds2  12570  dvdscmul  12571  dvdsmulc  12572  dvdstr  12578  spwpr4  14356  domneq0  16054  aspid  16086  znleval2  16525  concompss  17175  islly2  17226  elmptrab2  17539  lmmcvg  18703  ivthicc  18834  aaliou3lem7  19745  logimcl  19943  qrngdiv  20789  ajfuni  21454  funadj  22482  fovcld  23218  modaddabs  24026  ax5seg  24638  cgr3permute1  24743  cgr3com  24748  brifs2  24773  idinside  24779  btwnconn1  24796  lineunray  24842  eqfnung2  25221  cur1val  25301  grpodivzer  25480  ismonb2  25915  cmpmon  25918  isepib2  25925  pm13.194  27715  fmulcl  27814  fmuldfeqlem1  27815  stoweidlem17  27869  stoweidlem31  27883  stowei  27916  sigaraf  27946  sigarmf  27947  constr3pthlem2  28402  bnj1098  29131  bnj546  29244  bnj998  29304  bnj1006  29307  bnj1173  29348  bnj1189  29355  lsatlspsn2  29804  3dim2  30279  paddasslem14  30644  4atexlemex6  30885  cdlemg10bALTN  31447  cdlemg44  31544  tendoplcl  31592  hdmap14lem14  32696
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator