Theorem 3ancoma 1109

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  3anrot  1111  3anrev  1112  cadcomb  1632  f13dfv  7252  suppssfifsupp  9319  elfzmlbp  13637  elfzo2  13660  pythagtriplem2  16843  pythagtrip  16860  xpsfrnel  17582  fucinv  17999  setcinv  18113  rngcinv  20673  ringcinv  20707  xrsdsreclb  21453  ordthaus  23431  regr1lem2  23787  xmetrtri2  24403  clmvscom  25139  hlcomb  28759  nb3grpr2  29540  nb3gr2nb  29541  rusgrnumwwlkslem  30128  ablomuldiv  30711  nvscom  30788  cnvadj  32051  iocinif  32943  fzto1st  33243  psgnfzto1st  33245  bnj312  34968  cgr3permute1  36358  lineext  36386  colinbtwnle  36428  outsideofcom  36438  linecom  36460  linerflx2  36461  cdlemg33d  41293  uunT12p3  45337  ichexmpl2  48036  grtriproplem  48521  grtrif1o  48524  rngcinvALTV  48858  ringcinvALTV  48892