Theorem 3ancoma 1094

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 1092	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2		3anass 1091	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4i 280	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

Syntax hints:   ↔ wb 208   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3anrot  1096  3anrev  1097  cadcomb  1614  f13dfv  7031  suppssfifsupp  8848  elfzmlbp  13019  elfzo2  13042  pythagtriplem2  16154  pythagtrip  16171  xpsfrnel  16835  fucinv  17243  setcinv  17350  xrsdsreclb  20592  ordthaus  21992  regr1lem2  22348  xmetrtri2  22966  clmvscom  23694  hlcomb  26389  nb3grpr2  27165  nb3gr2nb  27166  rusgrnumwwlkslem  27748  ablomuldiv  28329  nvscom  28406  cnvadj  29669  iocinif  30504  fzto1st  30745  psgnfzto1st  30747  bnj312  31982  cgr3permute1  33509  lineext  33537  colinbtwnle  33579  outsideofcom  33589  linecom  33611  linerflx2  33612  cdlemg33d  37860  uunT12p3  41156  ichexmpl2  43652  rngcinv  44272  rngcinvALTV  44284  ringcinv  44323  ringcinvALTV  44347