Theorem 3ancoma 1099

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3anrot  1101  3anrev  1102  cadcomb  1615  f13dfv  7272  suppssfifsupp  9378  elfzmlbp  13612  elfzo2  13635  pythagtriplem2  16750  pythagtrip  16767  xpsfrnel  17508  fucinv  17926  setcinv  18040  xrsdsreclb  20992  ordthaus  22888  regr1lem2  23244  xmetrtri2  23862  clmvscom  24606  hlcomb  27885  nb3grpr2  28671  nb3gr2nb  28672  rusgrnumwwlkslem  29254  ablomuldiv  29836  nvscom  29913  cnvadj  31176  iocinif  32023  fzto1st  32293  psgnfzto1st  32295  bnj312  33754  cgr3permute1  35051  lineext  35079  colinbtwnle  35121  outsideofcom  35131  linecom  35153  linerflx2  35154  cdlemg33d  39628  uunT12p3  43611  ichexmpl2  46186  rngcinv  46927  rngcinvALTV  46939  ringcinv  46978  ringcinvALTV  47002