MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anan32 Structured version   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  5680  tz7.49c  6703  ispos2  14405  lbsacsbs  16228  obslbs  16957  leordtvallem1  17274  trfbas2  17875  lssbn  19304  sineq0  20429  dchrelbas3  21022  nb3grapr2  21463  elicoelioo  24141  cndprobprob  24696  elno3  25610  ellimits  25755  islbs4  27279  usg2wlkeq  28304  bnj543  29264
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