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

Theorem 3anan12 978
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 972 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
2 3anass 969 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ps  /\  ( ph  /\  ch )
) )
31, 2bitri 249 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  2reu5lem3  3268  fncnv  5585  dff1o2  5749  ixxun  11422  mreexexlem4d  14699  unocv  18225  iunocv  18226  mbfmax  21255  ulm2  21978  pridlnr  28979  usgra2wlkspthlem2  30440  wwlknprop  30463  wwlknfi  30513  eclclwwlkn1  30649  numclwwlkovf2  30820  numclwlk1lem2f1  30830  sineq0ALT  31986  bnj548  32203
  Copyright terms: Public domain W3C validator