Theorem 3ancoma 1097

Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 5-Jun-2022.)

Assertion

Ref	Expression
3ancoma	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

Proof of Theorem 3ancoma

Step	Hyp	Ref	Expression
1		3anan12 1095	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2		3anass 1094	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4i 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anrot  1099  3anrev  1100  cadcomb  1613  f13dfv  7215  suppssfifsupp  9289  elfzmlbp  13560  elfzo2  13583  pythagtriplem2  16747  pythagtrip  16764  xpsfrnel  17484  fucinv  17901  setcinv  18015  rngcinv  20540  ringcinv  20574  xrsdsreclb  21338  ordthaus  23287  regr1lem2  23643  xmetrtri2  24260  clmvscom  25006  hlcomb  28566  nb3grpr2  29346  nb3gr2nb  29347  rusgrnumwwlkslem  29932  ablomuldiv  30514  nvscom  30591  cnvadj  31854  iocinif  32737  fzto1st  33058  psgnfzto1st  33060  bnj312  34681  cgr3permute1  36024  lineext  36052  colinbtwnle  36094  outsideofcom  36104  linecom  36126  linerflx2  36127  cdlemg33d  40691  uunT12p3  44778  ichexmpl2  47458  grtriproplem  47927  grtrif1o  47930  rngcinvALTV  48264  ringcinvALTV  48298