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  7274  suppssfifsupp  9356  elfzmlbp  13753  elfzo2  13776  pythagtriplem2  16975  pythagtrip  16992  xpsfrnel  17714  fucinv  18131  setcinv  18245  rngcinv  20869  ringcinv  20903  xrsdsreclb  21700  ordthaus  23682  regr1lem2  24039  xmetrtri2  24655  clmvscom  25391  hlcomb  29051  nb3grpr2  29946  nb3gr2nb  29947  rusgrnumwwlkslem  30543  ablomuldiv  31136  nvscom  31213  cnvadj  32476  iocinif  33355  fzto1st  33646  psgnfzto1st  33648  bnj312  35326  cgr3permute1  36783  lineext  36811  colinbtwnle  36853  outsideofcom  36863  linecom  36885  linerflx2  36886  cdlemg33d  41734  uunT12p3  45743  ichexmpl2  48496  grtriproplem  48981  grtrif1o  48984  rngcinvALTV  49317  ringcinvALTV  49351