Theorem 3ancoma 1115

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 1112	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2		3anass 1111	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4i 281	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3anrot  1117  3anrev  1118  cadcomb  1643  f13dfv  7274  suppssfifsupp  9341  elfzmlbp  13669  elfzo2  13692  pythagtriplem2  16878  pythagtrip  16895  xpsfrnel  17617  fucinv  18034  setcinv  18148  rngcinv  20723  ringcinv  20757  xrsdsreclb  21545  ordthaus  23522  regr1lem2  23878  xmetrtri2  24494  clmvscom  25230  hlcomb  28856  nb3grpr2  29714  nb3gr2nb  29715  rusgrnumwwlkslem  30302  ablomuldiv  30885  nvscom  30962  cnvadj  32225  iocinif  33107  fzto1st  33404  psgnfzto1st  33406  bnj312  35082  cgr3permute1  36521  lineext  36549  colinbtwnle  36591  outsideofcom  36601  linecom  36623  linerflx2  36624  cdlemg33d  41464  uunT12p3  45493  ichexmpl2  48202  grtriproplem  48687  grtrif1o  48690  rngcinvALTV  49024  ringcinvALTV  49058