Theorem 3ancoma 1096

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 1094	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2		3anass 1093	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4i 277	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  3anrot  1098  3anrev  1099  cadcomb  1616  f13dfv  7127  suppssfifsupp  9073  elfzmlbp  13296  elfzo2  13319  pythagtriplem2  16446  pythagtrip  16463  xpsfrnel  17190  fucinv  17607  setcinv  17721  xrsdsreclb  20557  ordthaus  22443  regr1lem2  22799  xmetrtri2  23417  clmvscom  24159  hlcomb  26868  nb3grpr2  27653  nb3gr2nb  27654  rusgrnumwwlkslem  28235  ablomuldiv  28815  nvscom  28892  cnvadj  30155  iocinif  31004  fzto1st  31272  psgnfzto1st  31274  bnj312  32591  cgr3permute1  34277  lineext  34305  colinbtwnle  34347  outsideofcom  34357  linecom  34379  linerflx2  34380  cdlemg33d  38650  uunT12p3  42311  ichexmpl2  44810  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502