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

Theorem 3anan32 948
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 938 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 an32 774 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )
31, 2bitri 241 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ch )  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    /\ w3a 936
This theorem is referenced by:  dff1o3  5639  tz7.49c  6662  ispos2  14360  lbsacsbs  16183  obslbs  16912  leordtvallem1  17228  trfbas2  17828  lssbn  19257  sineq0  20382  dchrelbas3  20975  nb3grapr2  21416  elicoelioo  24094  cndprobprob  24649  elno3  25523  ellimits  25664  islbs4  27170  bnj543  28970
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator