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

Theorem 3anan12 986
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 980 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
2 3anass 977 . 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 973
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 975
This theorem is referenced by:  2reu5lem3  3311  fncnv  5650  dff1o2  5819  ixxun  11541  mreexexlem4d  14898  unocv  18478  iunocv  18479  mbfmax  21791  ulm2  22514  usgra2wlkspthlem2  24296  wwlknprop  24362  wwlknfi  24414  eclclwwlkn1  24508  numclwwlkovf2  24761  numclwlk1lem2f1  24771  pridlnr  30036  sineq0ALT  32817  bnj548  33034
  Copyright terms: Public domain W3C validator