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

Theorem 3simpc 987
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 970 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
2 3simpa 985 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  ( ps  /\ 
ch ) )
31, 2sylbi 195 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  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:  simp3  990  3adant1  1006  3adantl1  1144  3adantr1  1147  eupickbOLD  2345  find  6499  tz7.49c  6899  eqsup  7704  mulcanenq  9127  elnpi  9155  divcan2  10000  diveq0  10002  divrec  10008  divcan3  10016  eliooord  11353  fzrev3  11520  modaddabs  11744  modaddmod  11745  modmulmod  11762  sqdiv  11929  swrdlend  12323  ccats1swrdeqbi  12387  sqrmo  12739  muldvds2  13556  dvdscmul  13557  dvdsmulc  13558  dvdstr  13564  domneq0  17367  aspid  17399  znleval2  17986  redvr  18045  1marepvmarrepid  18384  concompss  19035  islly2  19086  elmptrab2  19399  lmmcvg  20770  ivthicc  20940  aaliou3lem7  21813  logimcl  22019  qrngdiv  22871  ax5seg  23182  usgra2edg1  23300  constr2trl  23496  constr3trllem2  23535  constr3pthlem2  23540  ajfuni  24258  funadj  25288  fovcld  25953  trleile  26125  isinftm  26196  cgr3permute1  28077  cgr3com  28082  brifs2  28107  idinside  28113  btwnconn1  28130  lineunray  28176  wl-nfeqfb  28363  pm13.194  29663  fmulcl  29759  fmuldfeqlem1  29760  stoweidlem17  29809  stoweidlem31  29823  sigaraf  29886  sigarmf  29887  pr1eqbg  30118  elfzelfzlble  30206  spthdifv  30296  usgra2pth  30298  clwwlkfo  30456  clwwlknwwlkncl  30459  clwwisshclww  30468  clwlkfclwwlk  30514  rusgranumwlkg  30573  numclwwlkovgelim  30679  numclwwlk3  30699  zlmodzxzscm  30751  pmatcollpw1lem4  30899  bnj1098  31774  bnj546  31886  bnj998  31946  bnj1006  31949  bnj1173  31990  bnj1189  31997  riotasv2s  32606  lsatlspsn2  32634  3dim2  33109  paddasslem14  33474  4atexlemex6  33715  cdlemg10bALTN  34277  cdlemg44  34374  tendoplcl  34422  hdmap14lem14  35526
  Copyright terms: Public domain W3C validator