Theorem 3ancoma 1097

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086

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

This theorem is referenced by:  3anrot  1099  3anrev  1100  cadcomb  1613  f13dfv  7249  suppssfifsupp  9331  elfzmlbp  13600  elfzo2  13623  pythagtriplem2  16788  pythagtrip  16805  xpsfrnel  17525  fucinv  17938  setcinv  18052  rngcinv  20546  ringcinv  20580  xrsdsreclb  21330  ordthaus  23271  regr1lem2  23627  xmetrtri2  24244  clmvscom  24990  hlcomb  28530  nb3grpr2  29310  nb3gr2nb  29311  rusgrnumwwlkslem  29899  ablomuldiv  30481  nvscom  30558  cnvadj  31821  iocinif  32704  fzto1st  33060  psgnfzto1st  33062  bnj312  34702  cgr3permute1  36036  lineext  36064  colinbtwnle  36106  outsideofcom  36116  linecom  36138  linerflx2  36139  cdlemg33d  40703  uunT12p3  44791  ichexmpl2  47471  grtriproplem  47938  grtrif1o  47941  rngcinvALTV  48264  ringcinvALTV  48298