Theorem 3ancoma 1115

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 1112	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2		3anass 1111	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4i 281	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anrot  1117  3anrev  1118  cadcomb  1646  f13dfv  7283  suppssfifsupp  9350  elfzmlbp  13686  elfzo2  13709  pythagtriplem2  16902  pythagtrip  16919  xpsfrnel  17641  fucinv  18058  setcinv  18172  rngcinv  20773  ringcinv  20807  xrsdsreclb  21601  ordthaus  23578  regr1lem2  23934  xmetrtri2  24550  clmvscom  25286  hlcomb  28912  nb3grpr2  29770  nb3gr2nb  29771  rusgrnumwwlkslem  30358  ablomuldiv  30941  nvscom  31018  cnvadj  32281  iocinif  33163  fzto1st  33454  psgnfzto1st  33456  bnj312  35133  cgr3permute1  36561  lineext  36589  colinbtwnle  36631  outsideofcom  36641  linecom  36663  linerflx2  36664  cdlemg33d  41524  uunT12p3  45551  ichexmpl2  48260  grtriproplem  48745  grtrif1o  48748  rngcinvALTV  49082  ringcinvALTV  49116