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

Theorem 3anan12 950
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 944 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
2 3anass 941 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ps  /\  ( ph  /\  ch )
) )
31, 2bitri 242 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    /\ w3a 937
This theorem is referenced by:  2reu5lem3  3143  fncnv  5517  dff1o2  5681  ixxun  10934  mreexexlem4d  13874  unocv  16909  iunocv  16910  mbfmax  19543  ulm2  20303  pridlnr  26648  usgra2wlkspthlem2  28309  sineq0ALT  29051  bnj548  29270
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator