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

Theorem 3anan12 995
Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
3anan12  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ( ph  /\  ch ) ) )

Proof of Theorem 3anan12
StepHypRef Expression
1 3ancoma 989 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
2 3anass 986 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ps  /\  ( ph  /\  ch )
) )
31, 2bitri 252 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ 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:  an33rean  1378  2reu5lem3  3285  fncnv  5665  dff1o2  5836  ixxun  11651  mreexexlem4d  15504  unocv  19174  iunocv  19175  mbfmax  22482  ulm2  23205  usgra2wlkspthlem2  25193  wwlknprop  25259  wwlknfi  25311  eclclwwlkn1  25405  numclwwlkovf2  25657  numclwlk1lem2f1  25667  bnj548  29496  pridlnr  31973  sineq0ALT  36974  elbigo  39123
  Copyright terms: Public domain W3C validator