Theorem 3anan12 1051

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

Step	Hyp	Ref	Expression
1		3ancoma 1045	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ph /\ ch ) )
2		3anass 1042	. 2 |- ( ( ps /\ ph /\ ch ) <-> ( ps /\ ( ph /\ ch ) ) )
3	1, 2	bitri 264	1 |- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ( ph /\ ch ) ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  an33rean  1446  2reu5lem3  3415  snopeqop  4969  fncnv  5962  dff1o2  6142  ixxun  12191  elfz1b  12409  mreexexlem4d  16307  unocv  20024  iunocv  20025  iscvsp  22928  mbfmax  23416  ulm2  24139  iswwlks  26728  wwlksnfi  26801  eclclwwlksn1  26952  numclwlk1lem2f1  27227  bnj548  30967  pridlnr  33835  brres2  34035  sineq0ALT  39173  elbigo  42345