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

Theorem 3anan32 994
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 984 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 an32 805 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )
31, 2bitri 252 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ch )  /\  ps )
)
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:  anandi3r  997  dff1o3  5837  tz7.49c  7171  ispos2  16144  lbsacsbs  18314  obslbs  19224  islbs4  19321  leordtvallem1  20157  trfbas2  20789  lssbn  22212  sineq0  23341  dchrelbas3  24029  nb3grapr2  25027  usg2wlkeq  25281  elicoelioo  28196  cndprobprob  29097  bnj543  29492  elno3  30329  ellimits  30462
  Copyright terms: Public domain W3C validator