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

Theorem 3simpc 993
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 976 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
2 3simpa 991 . 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 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  simp3  996  3adant1  1012  3adantl1  1150  3adantr1  1153  find  6698  tz7.49c  7103  eqsup  7907  mulcanenq  9327  elnpi  9355  divcan2  10211  diveq0  10213  divrec  10219  divcan3  10227  eliooord  11587  fzrev3  11749  modaddabs  12016  modaddmod  12017  modmulmod  12034  sqdiv  12215  swrdlend  12647  swrdnd  12648  ccats1swrdeqbi  12714  sqrmo  13167  muldvds2  14093  dvdscmul  14094  dvdsmulc  14095  dvdstr  14102  funcestrcsetclem9  15616  funcsetcestrclem9  15631  domneq0  18141  aspid  18174  znleval2  18767  redvr  18826  scmatscmiddistr  19177  1marepvmarrepid  19244  mat2pmatghm  19398  pmatcollpw1lem1  19442  monmatcollpw  19447  pmatcollpwscmatlem2  19458  concompss  20100  islly2  20151  elmptrab2  20495  lmmcvg  21866  ivthicc  22036  aaliou3lem7  22911  logimcl  23123  qrngdiv  24007  ax5seg  24443  usgra2edg1  24585  constr2trl  24803  constr3trllem2  24853  constr3pthlem2  24858  clwwlkfo  24999  clwwlknwwlkncl  25002  clwwisshclww  25009  clwlkfclwwlk  25046  clwlkf1clwwlklem  25051  rusgranumwlkg  25160  numclwwlkovgelim  25291  numclwwlk3  25311  ajfuni  25973  funadj  27003  fovcld  27699  trleile  27888  isinftm  27959  cgr3permute1  29926  cgr3com  29931  brifs2  29956  idinside  29962  btwnconn1  29979  lineunray  30025  wl-nfeqfb  30230  pm13.194  31560  fmulcl  31814  fmuldfeqlem1  31815  stoweidlem17  32038  stoweidlem31  32052  sigaraf  32309  sigarmf  32310  ccats1pfxeqbi  32659  pr1eqbg  32671  elfzelfzlble  32711  spthdifv  32724  usgra2pth  32726  usg2edgneu  32784  funcringcsetcALTV2lem9  33106  funcringcsetclem9ALTV  33129  zlmodzxzscm  33200  divsub1dir  33376  elbigoimp  33431  digexp  33482  bnj1098  34243  bnj546  34355  bnj998  34415  bnj1006  34418  bnj1173  34459  bnj1189  34466  riotasv2s  35086  lsatlspsn2  35114  3dim2  35589  paddasslem14  35954  4atexlemex6  36195  cdlemg10bALTN  36759  cdlemg44  36856  tendoplcl  36904  hdmap14lem14  38008
  Copyright terms: Public domain W3C validator