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

Theorem 3simpc 1004
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 987 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
2 3simpa 1002 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  ( ps  /\ 
ch ) )
31, 2sylbi 198 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  simp3  1007  3adant1  1023  3adantl1  1161  3adantr1  1164  find  6732  tz7.49c  7171  eqsup  7976  mulcanenq  9384  elnpi  9412  divcan2  10277  diveq0  10279  divrec  10285  divcan3  10293  eliooord  11694  fzrev3  11859  modaddabs  12132  modaddmod  12133  muladdmodid  12134  modmulmod  12152  sqdiv  12337  swrdlend  12772  swrdnd  12773  ccats1swrdeqbi  12839  sqrmo  13294  muldvds2  14306  dvdscmul  14307  dvdsmulc  14308  dvdstr  14315  funcestrcsetclem9  15984  funcsetcestrclem9  15999  domneq0  18456  aspid  18489  znleval2  19057  redvr  19116  scmatscmiddistr  19464  1marepvmarrepid  19531  mat2pmatghm  19685  pmatcollpw1lem1  19729  monmatcollpw  19734  pmatcollpwscmatlem2  19745  concompss  20379  islly2  20430  elmptrab2  20774  lmmcvg  22124  ivthicc  22290  aaliou3lem7  23170  logimcl  23384  qrngdiv  24325  ax5seg  24814  usgra2edg1  24956  constr2trl  25174  constr3trllem2  25224  constr3pthlem2  25229  clwwlkfo  25370  clwwlknwwlkncl  25373  clwwisshclww  25380  clwlkfclwwlk  25417  clwlkf1clwwlklem  25422  rusgranumwlkg  25531  numclwwlkovgelim  25662  numclwwlk3  25682  ajfuni  26346  funadj  27374  fovcld  28079  trleile  28265  isinftm  28336  bnj1098  29383  bnj546  29495  bnj998  29555  bnj1006  29558  bnj1173  29599  bnj1189  29606  cgr3permute1  30600  cgr3com  30605  brifs2  30630  idinside  30636  btwnconn1  30653  lineunray  30699  wl-nfeqfb  31577  riotasv2s  32239  lsatlspsn2  32267  3dim2  32742  paddasslem14  33107  4atexlemex6  33348  cdlemg10bALTN  33912  cdlemg44  34009  tendoplcl  34057  hdmap14lem14  35161  pm13.194  36400  fmulcl  37231  fmuldfeqlem1  37232  stoweidlem17  37446  stoweidlem31  37461  sigaraf  37862  sigarmf  37863  ccats1pfxeqbi  38371  pr1eqbg  38383  elfzelfzlble  38419  spthdifv  38431  usgra2pth  38433  usg2edgneu  38491  funcringcsetcALTV2lem9  38813  funcringcsetclem9ALTV  38836  zlmodzxzscm  38907  divsub1dir  39083  elbigoimp  39137  digexp  39188
  Copyright terms: Public domain W3C validator