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  7308  suppssfifsupp  9402  elfzmlbp  13803  elfzo2  13826  pythagtriplem2  17027  pythagtrip  17044  xpsfrnel  17766  fucinv  18183  setcinv  18297  rngcinv  20922  ringcinv  20956  xrsdsreclb  21753  ordthaus  23735  regr1lem2  24092  xmetrtri2  24708  clmvscom  25444  hlcomb  29102  nb3grpr2  29997  nb3gr2nb  29998  rusgrnumwwlkslem  30594  ablomuldiv  31187  nvscom  31264  cnvadj  32527  iocinif  33446  fzto1st  33740  psgnfzto1st  33742  bnj312  35426  cgr3permute1  37004  lineext  37032  colinbtwnle  37074  outsideofcom  37084  linecom  37106  linerflx2  37107  cdlemg33d  41969  uunT12p3  45986  ichexmpl2  48767  grtriproplem  49252  grtrif1o  49255  rngcinvALTV  49588  ringcinvALTV  49622