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  7252  suppssfifsupp  9338  elfzmlbp  13607  elfzo2  13630  pythagtriplem2  16795  pythagtrip  16812  xpsfrnel  17532  fucinv  17945  setcinv  18059  rngcinv  20553  ringcinv  20587  xrsdsreclb  21337  ordthaus  23278  regr1lem2  23634  xmetrtri2  24251  clmvscom  24997  hlcomb  28537  nb3grpr2  29317  nb3gr2nb  29318  rusgrnumwwlkslem  29906  ablomuldiv  30488  nvscom  30565  cnvadj  31828  iocinif  32711  fzto1st  33067  psgnfzto1st  33069  bnj312  34709  cgr3permute1  36043  lineext  36071  colinbtwnle  36113  outsideofcom  36123  linecom  36145  linerflx2  36146  cdlemg33d  40710  uunT12p3  44798  ichexmpl2  47475  grtriproplem  47942  grtrif1o  47945  rngcinvALTV  48268  ringcinvALTV  48302