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  27854  nb3grpr2  28640  nb3gr2nb  28641  rusgrnumwwlkslem  29223  ablomuldiv  29805  nvscom  29882  cnvadj  31145  iocinif  31992  fzto1st  32262  psgnfzto1st  32264  bnj312  33723  cgr3permute1  35020  lineext  35048  colinbtwnle  35090  outsideofcom  35100  linecom  35122  linerflx2  35123  cdlemg33d  39580  uunT12p3  43563  ichexmpl2  46138  rngcinv  46879  rngcinvALTV  46891  ringcinv  46930  ringcinvALTV  46954