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  1610  f13dfv  7294  suppssfifsupp  9418  elfzmlbp  13676  elfzo2  13699  pythagtriplem2  16851  pythagtrip  16868  xpsfrnel  17609  fucinv  18030  setcinv  18144  rngcinv  20654  ringcinv  20688  xrsdsreclb  21449  ordthaus  23408  regr1lem2  23764  xmetrtri2  24382  clmvscom  25137  hlcomb  28626  nb3grpr2  29415  nb3gr2nb  29416  rusgrnumwwlkslem  29999  ablomuldiv  30581  nvscom  30658  cnvadj  31921  iocinif  32790  fzto1st  33106  psgnfzto1st  33108  bnj312  34705  cgr3permute1  36030  lineext  36058  colinbtwnle  36100  outsideofcom  36110  linecom  36132  linerflx2  36133  cdlemg33d  40692  uunT12p3  44800  ichexmpl2  47395  grtriproplem  47844  grtrif1o  47847  rngcinvALTV  48120  ringcinvALTV  48154