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  7272  suppssfifsupp  9397  elfzmlbp  13661  elfzo2  13684  pythagtriplem2  16842  pythagtrip  16859  xpsfrnel  17581  fucinv  17994  setcinv  18108  rngcinv  20602  ringcinv  20636  xrsdsreclb  21386  ordthaus  23327  regr1lem2  23683  xmetrtri2  24300  clmvscom  25046  hlcomb  28587  nb3grpr2  29367  nb3gr2nb  29368  rusgrnumwwlkslem  29956  ablomuldiv  30538  nvscom  30615  cnvadj  31878  iocinif  32763  fzto1st  33119  psgnfzto1st  33121  bnj312  34748  cgr3permute1  36071  lineext  36099  colinbtwnle  36141  outsideofcom  36151  linecom  36173  linerflx2  36174  cdlemg33d  40733  uunT12p3  44793  ichexmpl2  47451  grtriproplem  47918  grtrif1o  47921  rngcinvALTV  48218  ringcinvALTV  48252