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

Theorem 3anass 982
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 980 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 anass 401 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
31, 2bitri 184 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  3anrot  983  3anan12  990  anandi3  991  3exdistr  1915  r3al  2521  ceqsex2  2777  ceqsex3v  2779  ceqsex4v  2780  ceqsex6v  2781  ceqsex8v  2782  eldifpr  3618  rexdifpr  3619  trel3  4106  sowlin  4316  dff1o4  5464  mpoxopovel  6235  dfsmo2  6281  ecopovtrn  6625  ecopovtrng  6628  elixp2  6695  elixp  6698  mptelixpg  6727  eqinfti  7012  distrnqg  7364  recmulnqg  7368  ltexnqq  7385  enq0tr  7411  distrnq0  7436  genpdflem  7484  distrlem1prl  7559  distrlem1pru  7560  divmulasscomap  8629  muldivdirap  8640  divmuldivap  8645  prime  9328  eluz2  9510  raluz2  9555  elixx1  9871  elixx3g  9875  elioo2  9895  elioo5  9907  elicc4  9914  iccneg  9963  icoshft  9964  elfz1  9987  elfz  9988  elfz2  9989  elfzm11  10064  elfz2nn0  10085  elfzo2  10123  elfzo3  10136  lbfzo0  10154  fzind2  10212  zmodid2  10325  redivap  10854  imdivap  10861  maxleast  11193  cosmul  11724  dfgcd2  11985  lcmneg  12044  coprmgcdb  12058  divgcdcoprmex  12072  cncongr1  12073  cncongr2  12074  difsqpwdvds  12307  elgz  12339  mgmsscl  12659  ismhm  12730  mhmpropd  12734  issubm  12740  issrg  12961  srglmhm  12989  srgrmhm  12990  isring  12996  lmbrf  13348  uptx  13407  txcn  13408  xmetec  13570  bl2ioo  13675  lgsmodeq  14079  lgsmulsqcoprm  14080  findset  14319
  Copyright terms: Public domain W3C validator