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  1613  f13dfv  7294  suppssfifsupp  9420  elfzmlbp  13679  elfzo2  13702  pythagtriplem2  16855  pythagtrip  16872  xpsfrnel  17607  fucinv  18021  setcinv  18135  rngcinv  20637  ringcinv  20671  xrsdsreclb  21431  ordthaus  23392  regr1lem2  23748  xmetrtri2  24366  clmvscom  25123  hlcomb  28611  nb3grpr2  29400  nb3gr2nb  29401  rusgrnumwwlkslem  29989  ablomuldiv  30571  nvscom  30648  cnvadj  31911  iocinif  32783  fzto1st  33123  psgnfzto1st  33125  bnj312  34726  cgr3permute1  36049  lineext  36077  colinbtwnle  36119  outsideofcom  36129  linecom  36151  linerflx2  36152  cdlemg33d  40711  uunT12p3  44822  ichexmpl2  47457  grtriproplem  47906  grtrif1o  47909  rngcinvALTV  48192  ringcinvALTV  48226