Theorem 3ancoma 1098

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 1096	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2		3anass 1095	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4i 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

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

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 1089

This theorem is referenced by:  3anrot  1100  3anrev  1101  cadcomb  1610  f13dfv  7310  suppssfifsupp  9449  elfzmlbp  13696  elfzo2  13719  pythagtriplem2  16864  pythagtrip  16881  xpsfrnel  17622  fucinv  18043  setcinv  18157  rngcinv  20659  ringcinv  20693  xrsdsreclb  21454  ordthaus  23413  regr1lem2  23769  xmetrtri2  24387  clmvscom  25142  hlcomb  28629  nb3grpr2  29418  nb3gr2nb  29419  rusgrnumwwlkslem  30002  ablomuldiv  30584  nvscom  30661  cnvadj  31924  iocinif  32786  fzto1st  33096  psgnfzto1st  33098  bnj312  34688  cgr3permute1  36012  lineext  36040  colinbtwnle  36082  outsideofcom  36092  linecom  36114  linerflx2  36115  cdlemg33d  40666  uunT12p3  44773  ichexmpl2  47344  grtriproplem  47790  grtrif1o  47793  rngcinvALTV  47999  ringcinvALTV  48033