Theorem 3anass 938

Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
3anass	|- ((ph /\ ps /\ ch) <-> (ph /\ (ps /\ ch)))

Proof of Theorem 3anass

Step	Hyp	Ref	Expression
1		df-3an 936	. 2 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		anass 630	. 2 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))
3	1, 2	bitri 240	1 |- ((ph /\ ps /\ ch) <-> (ph /\ (ps /\ ch)))

Syntax hints:   <-> wb 176   /\ wa 358   /\ w3a 934

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 177  df-an 360  df-3an 936

This theorem is referenced by:  3anrot  939  3anan12  947  3exdistr  1910  r3al  2671  ceqsex2  2895  ceqsex3v  2897  ceqsex4v  2898  ceqsex6v  2899  ceqsex8v  2900  2reu5lem1  3041  2reu5lem2  3042  2reu5lem3  3043  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  setconslem1  4731  dff1o2  5291  dff1o4  5294  dmsi  5519  ndmovass  5618  ndmovdistr  5619  brsnsi1  5775  brsnsi2  5776  brtxp  5783  restxp  5786  oqelins4  5794  dmtxp  5802  brpprod  5839  dmpprod  5840  xpassenlem  6056  xpassen  6057  ceex  6174  ce0nnul  6177  spacind  6287