Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  3anass GIF version

Theorem 3anass 889
 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 887 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 anass 381 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
31, 2bitri 173 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98   ∧ w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  3anrot  890  3anan12  897  anandi3  898  3exdistr  1792  r3al  2366  ceqsex2  2594  ceqsex3v  2596  ceqsex4v  2597  ceqsex6v  2598  ceqsex8v  2599  trel3  3862  sowlin  4057  dff1o4  5134  mpt2xopovel  5856  dfsmo2  5902  ecopovtrn  6203  ecopovtrng  6206  distrnqg  6485  recmulnqg  6489  ltexnqq  6506  enq0tr  6532  distrnq0  6557  genpdflem  6605  distrlem1prl  6680  distrlem1pru  6681  divmuldivap  7688  prime  8337  eluz2  8479  raluz2  8522  elixx1  8766  elixx3g  8770  elioo2  8790  elioo5  8802  elicc4  8809  iccneg  8857  icoshft  8858  elfz1  8879  elfz  8880  elfz2  8881  elfzm11  8953  elfz2nn0  8973  elfzo2  9007  elfzo3  9019  lbfzo0  9037  fzind2  9095  redivap  9474  imdivap  9481  findset  10070
 Copyright terms: Public domain W3C validator