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  1614  f13dfv  7208  suppssfifsupp  9264  elfzmlbp  13539  elfzo2  13562  pythagtriplem2  16729  pythagtrip  16746  xpsfrnel  17466  fucinv  17883  setcinv  17997  rngcinv  20553  ringcinv  20587  xrsdsreclb  21351  ordthaus  23300  regr1lem2  23656  xmetrtri2  24272  clmvscom  25018  hlcomb  28582  nb3grpr2  29362  nb3gr2nb  29363  rusgrnumwwlkslem  29948  ablomuldiv  30530  nvscom  30607  cnvadj  31870  iocinif  32762  fzto1st  33070  psgnfzto1st  33072  bnj312  34722  cgr3permute1  36088  lineext  36116  colinbtwnle  36158  outsideofcom  36168  linecom  36190  linerflx2  36191  cdlemg33d  40754  uunT12p3  44840  ichexmpl2  47507  grtriproplem  47976  grtrif1o  47979  rngcinvALTV  48313  ringcinvALTV  48347