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

Theorem 3simpc 956
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 941 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
2 3simpa 954 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  ( ps  /\ 
ch ) )
31, 2sylbi 188 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simp3  959  3adant1  975  3adantl1  1113  3adantr1  1116  eupickb  2346  find  4870  riotasv2s  6596  tz7.49c  6703  eqsup  7461  mulcanenq  8837  elnpi  8865  divcan2  9686  diveq0  9688  divrec  9694  divcan3  9702  eliooord  10970  fzrev3  11111  sqdiv  11447  sqrmo  12057  muldvds2  12875  dvdscmul  12876  dvdsmulc  12877  dvdstr  12883  spwpr4  14663  domneq0  16357  aspid  16389  znleval2  16836  concompss  17496  islly2  17547  elmptrab2  17860  lmmcvg  19214  ivthicc  19355  aaliou3lem7  20266  logimcl  20467  qrngdiv  21318  usgra2edg1  21403  constr2trl  21599  constr3trllem2  21638  constr3pthlem2  21643  ajfuni  22361  funadj  23389  fovcld  24050  isinftm  24251  redvr  24277  modaddabs  25115  ax5seg  25877  cgr3permute1  25982  cgr3com  25987  brifs2  26012  idinside  26018  btwnconn1  26035  lineunray  26081  pm13.194  27589  fmulcl  27687  fmuldfeqlem1  27688  stoweidlem17  27742  stoweidlem31  27756  sigaraf  27819  sigarmf  27820  pr1eqbg  28056  modaddmod  28153  modmulmod  28157  swrdltnd  28181  cshweqdifid  28272  spthdifv  28309  usgra2pth  28311  bnj1098  29154  bnj546  29267  bnj998  29327  bnj1006  29330  bnj1173  29371  bnj1189  29378  lsatlspsn2  29790  3dim2  30265  paddasslem14  30630  4atexlemex6  30871  cdlemg10bALTN  31433  cdlemg44  31530  tendoplcl  31578  hdmap14lem14  32682
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