Theorem 3ancoma 1103

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 1101	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2		3anass 1100	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4i 279	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3anrot  1105  3anrev  1106  cadcomb  1620  f13dfv  7225  suppssfifsupp  9290  elfzmlbp  13591  elfzo2  13614  pythagtriplem2  16786  pythagtrip  16803  xpsfrnel  17524  fucinv  17941  setcinv  18055  rngcinv  20616  ringcinv  20650  xrsdsreclb  21396  ordthaus  23374  regr1lem2  23730  xmetrtri2  24346  clmvscom  25082  hlcomb  28696  nb3grpr2  29477  nb3gr2nb  29478  rusgrnumwwlkslem  30065  ablomuldiv  30648  nvscom  30725  cnvadj  31988  iocinif  32880  fzto1st  33191  psgnfzto1st  33193  bnj312  34902  cgr3permute1  36283  lineext  36311  colinbtwnle  36353  outsideofcom  36363  linecom  36385  linerflx2  36386  cdlemg33d  41208  uunT12p3  45252  ichexmpl2  47952  grtriproplem  48437  grtrif1o  48440  rngcinvALTV  48774  ringcinvALTV  48808