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

Theorem 3anan32 946
Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Assertion
Ref Expression
3anan32  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ch )  /\  ps )
)

Proof of Theorem 3anan32
StepHypRef Expression
1 df-3an 936 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 an32 773 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )
31, 2bitri 240 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ch )  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    /\ w3a 934
This theorem is referenced by:  dff1o3  5494  tz7.49c  6474  ispos2  14098  lbsacsbs  15925  obslbs  16646  leordtvallem1  16956  trfbas2  17554  lssbn  18789  sineq0  19905  dchrelbas3  20493  elicoelioo  23286  cndprobprob  23656  elno3  24380  ellimits  24521  dfdir2  25394  islbs4  27405  nb3grapr2  28290  bnj543  29241
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator