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  7279  suppssfifsupp  9354  elfzmlbp  13698  elfzo2  13721  pythagtriplem2  16915  pythagtrip  16932  xpsfrnel  17654  fucinv  18071  setcinv  18185  rngcinv  20805  ringcinv  20839  xrsdsreclb  21633  ordthaus  23615  regr1lem2  23972  xmetrtri2  24588  clmvscom  25324  hlcomb  28956  nb3grpr2  29851  nb3gr2nb  29852  rusgrnumwwlkslem  30448  ablomuldiv  31041  nvscom  31118  cnvadj  32381  iocinif  33260  fzto1st  33551  psgnfzto1st  33553  bnj312  35230  cgr3permute1  36636  lineext  36664  colinbtwnle  36706  outsideofcom  36716  linecom  36738  linerflx2  36739  cdlemg33d  41590  uunT12p3  45632  ichexmpl2  48378  grtriproplem  48863  grtrif1o  48866  rngcinvALTV  49199  ringcinvALTV  49233