Theorem 3ancoma 1104

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 1102	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2		3anass 1101	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4i 280	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

Syntax hints:   ↔ wb 208   ∧ wa 397   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  3anrot  1106  3anrev  1107  cadcomb  1621  f13dfv  7221  suppssfifsupp  9287  elfzmlbp  13588  elfzo2  13611  pythagtriplem2  16783  pythagtrip  16800  xpsfrnel  17521  fucinv  17938  setcinv  18052  rngcinv  20612  ringcinv  20646  xrsdsreclb  21392  ordthaus  23370  regr1lem2  23726  xmetrtri2  24342  clmvscom  25078  hlcomb  28691  nb3grpr2  29472  nb3gr2nb  29473  rusgrnumwwlkslem  30060  ablomuldiv  30643  nvscom  30720  cnvadj  31983  iocinif  32875  fzto1st  33186  psgnfzto1st  33188  bnj312  34908  cgr3permute1  36289  lineext  36317  colinbtwnle  36359  outsideofcom  36369  linecom  36391  linerflx2  36392  cdlemg33d  41214  uunT12p3  45258  ichexmpl2  47957  grtriproplem  48442  grtrif1o  48445  rngcinvALTV  48779  ringcinvALTV  48813