New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  3anass GIF version

Theorem 3anass 938
 Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
3anass ((φ ψ χ) ↔ (φ (ψ χ)))

Proof of Theorem 3anass
StepHypRef Expression
1 df-3an 936 . 2 ((φ ψ χ) ↔ ((φ ψ) χ))
2 anass 630 . 2 (((φ ψ) χ) ↔ (φ (ψ χ)))
31, 2bitri 240 1 ((φ ψ χ) ↔ (φ (ψ χ)))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator