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  1615  f13dfv  7230  suppssfifsupp  9295  elfzmlbp  13567  elfzo2  13590  pythagtriplem2  16757  pythagtrip  16774  xpsfrnel  17495  fucinv  17912  setcinv  18026  rngcinv  20582  ringcinv  20616  xrsdsreclb  21380  ordthaus  23340  regr1lem2  23696  xmetrtri2  24312  clmvscom  25058  hlcomb  28687  nb3grpr2  29468  nb3gr2nb  29469  rusgrnumwwlkslem  30057  ablomuldiv  30639  nvscom  30716  cnvadj  31979  iocinif  32871  fzto1st  33196  psgnfzto1st  33198  bnj312  34888  cgr3permute1  36261  lineext  36289  colinbtwnle  36331  outsideofcom  36341  linecom  36363  linerflx2  36364  cdlemg33d  41082  uunT12p3  45154  ichexmpl2  47827  grtriproplem  48296  grtrif1o  48299  rngcinvALTV  48633  ringcinvALTV  48667