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  2208  find  4681  riotasv2s  6351  tz7.49c  6458  eqsup  7207  mulcanenq  8584  elnpi  8612  divcan2  9432  diveq0  9434  divrec  9440  divcan3  9448  eliooord  10710  fzrev3  10849  sqdiv  11169  sqrmo  11737  muldvds2  12554  dvdscmul  12555  dvdsmulc  12556  dvdstr  12562  spwpr4  14340  domneq0  16038  aspid  16070  znleval2  16509  concompss  17159  islly2  17210  elmptrab2  17523  lmmcvg  18687  ivthicc  18818  aaliou3lem7  19729  logimcl  19927  qrngdiv  20773  ajfuni  21438  funadj  22466  fovcld  23203  modaddabs  24011  ax5seg  24566  cgr3permute1  24671  cgr3com  24676  brifs2  24701  idinside  24707  btwnconn1  24724  lineunray  24770  eqfnung2  25118  cur1val  25198  grpodivzer  25377  ismonb2  25812  cmpmon  25815  isepib2  25822  pm13.194  27612  fmulcl  27711  fmuldfeqlem1  27712  stoweidlem17  27766  stoweidlem31  27780  stowei  27813  sigaraf  27843  sigarmf  27844  bnj1098  28815  bnj546  28928  bnj998  28988  bnj1006  28991  bnj1173  29032  bnj1189  29039  lsatlspsn2  29182  3dim2  29657  paddasslem14  30022  4atexlemex6  30263  cdlemg10bALTN  30825  cdlemg44  30922  tendoplcl  30970  hdmap14lem14  32074
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