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

Theorem 3simpc 1005
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 988 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
2 3simpa 1003 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  ( ps  /\ 
ch ) )
31, 2sylbi 199 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  simp3  1008  3adant1  1024  3adantl1  1162  3adantr1  1165  find  6738  tz7.49c  7180  eqsup  7985  fimin2g  8028  mulcanenq  9398  elnpi  9426  divcan2  10291  diveq0  10293  divrec  10299  divcan3  10307  eliooord  11707  fzrev3  11874  modaddabs  12147  modaddmod  12148  muladdmodid  12149  modmulmod  12167  sqdiv  12352  swrdlend  12795  swrdnd  12796  ccats1swrdeqbi  12862  sqrmo  13321  muldvds2  14333  dvdscmul  14334  dvdsmulc  14335  dvdstr  14342  funcestrcsetclem9  16038  funcsetcestrclem9  16053  domneq0  18526  aspid  18559  znleval2  19130  redvr  19189  scmatscmiddistr  19537  1marepvmarrepid  19604  mat2pmatghm  19758  pmatcollpw1lem1  19802  monmatcollpw  19807  pmatcollpwscmatlem2  19818  concompss  20452  islly2  20503  elmptrab2  20847  lmmcvg  22235  ivthicc  22413  aaliou3lem7  23309  logimcl  23523  qrngdiv  24466  ax5seg  24972  usgra2edg1  25114  constr2trl  25333  constr3trllem2  25383  constr3pthlem2  25388  clwwlkfo  25529  clwwlknwwlkncl  25532  clwwisshclww  25539  clwlkfclwwlk  25576  clwlkf1clwwlklem  25581  rusgranumwlkg  25690  numclwwlkovgelim  25821  numclwwlk3  25841  ajfuni  26505  funadj  27543  fovcld  28247  trleile  28440  isinftm  28511  bnj1098  29609  bnj546  29721  bnj998  29781  bnj1006  29784  bnj1173  29825  bnj1189  29832  cgr3permute1  30826  cgr3com  30831  brifs2  30856  idinside  30862  btwnconn1  30879  lineunray  30925  wl-nfeqfb  31840  riotasv2s  32505  lsatlspsn2  32533  3dim2  33008  paddasslem14  33373  4atexlemex6  33614  cdlemg10bALTN  34178  cdlemg44  34275  tendoplcl  34323  hdmap14lem14  35427  pm13.194  36739  fmulcl  37605  fmuldfeqlem1  37606  stoweidlem17  37823  stoweidlem31  37838  sigaraf  38339  sigarmf  38340  ccats1pfxeqbi  38848  pr1eqbg  38863  elfzelfzlble  38920  spthdifv  39283  usgra2pth  39285  usg2edgneu  39341  funcringcsetcALTV2lem9  39663  funcringcsetclem9ALTV  39686  zlmodzxzscm  39757  divsub1dir  39933  elbigoimp  39986  digexp  40037
  Copyright terms: Public domain W3C validator