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

Theorem 3simpc 995
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 978 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
2 3simpa 993 . 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 973
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
This theorem is referenced by:  simp3  998  3adant1  1014  3adantl1  1152  3adantr1  1155  eupickbOLD  2367  find  6709  tz7.49c  7111  eqsup  7916  mulcanenq  9338  elnpi  9366  divcan2  10215  diveq0  10217  divrec  10223  divcan3  10231  eliooord  11584  fzrev3  11745  modaddabs  12002  modaddmod  12003  modmulmod  12020  sqdiv  12201  swrdlend  12619  ccats1swrdeqbi  12686  sqrmo  13048  muldvds2  13870  dvdscmul  13871  dvdsmulc  13872  dvdstr  13878  domneq0  17745  aspid  17778  znleval2  18389  redvr  18448  scmatscmiddistr  18805  1marepvmarrepid  18872  mat2pmatghm  19026  pmatcollpw1lem1  19070  monmatcollpw  19075  pmatcollpwscmatlem2  19086  concompss  19728  islly2  19779  elmptrab2  20092  lmmcvg  21463  ivthicc  21633  aaliou3lem7  22507  logimcl  22713  qrngdiv  23565  ax5seg  23945  usgra2edg1  24087  constr2trl  24305  constr3trllem2  24355  constr3pthlem2  24360  clwwlkfo  24501  clwwlknwwlkncl  24504  clwwisshclww  24511  clwlkfclwwlk  24548  rusgranumwlkg  24662  numclwwlkovgelim  24794  numclwwlk3  24814  ajfuni  25479  funadj  26509  fovcld  27179  trleile  27344  isinftm  27415  cgr3permute1  29303  cgr3com  29308  brifs2  29333  idinside  29339  btwnconn1  29356  lineunray  29402  wl-nfeqfb  29595  pm13.194  30925  fmulcl  31159  fmuldfeqlem1  31160  stoweidlem17  31345  stoweidlem31  31359  sigaraf  31565  sigarmf  31566  pr1eqbg  31792  elfzelfzlble  31832  spthdifv  31847  usgra2pth  31849  usg2edgneu  31907  zlmodzxzscm  32042  bnj1098  32939  bnj546  33051  bnj998  33111  bnj1006  33114  bnj1173  33155  bnj1189  33162  riotasv2s  33779  lsatlspsn2  33807  3dim2  34282  paddasslem14  34647  4atexlemex6  34888  cdlemg10bALTN  35450  cdlemg44  35547  tendoplcl  35595  hdmap14lem14  36699
  Copyright terms: Public domain W3C validator