Theorem 3ancoma 1098

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

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

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 1089

This theorem is referenced by:  3anrot  1100  3anrev  1101  cadcomb  1615  f13dfv  7229  suppssfifsupp  9293  elfzmlbp  13593  elfzo2  13616  pythagtriplem2  16788  pythagtrip  16805  xpsfrnel  17526  fucinv  17943  setcinv  18057  rngcinv  20614  ringcinv  20648  xrsdsreclb  21394  ordthaus  23349  regr1lem2  23705  xmetrtri2  24321  clmvscom  25057  hlcomb  28671  nb3grpr2  29452  nb3gr2nb  29453  rusgrnumwwlkslem  30040  ablomuldiv  30623  nvscom  30700  cnvadj  31963  iocinif  32854  fzto1st  33164  psgnfzto1st  33166  bnj312  34855  cgr3permute1  36230  lineext  36258  colinbtwnle  36300  outsideofcom  36310  linecom  36332  linerflx2  36333  cdlemg33d  41155  uunT12p3  45228  ichexmpl2  47930  grtriproplem  48415  grtrif1o  48418  rngcinvALTV  48752  ringcinvALTV  48786