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  1614  f13dfv  7220  suppssfifsupp  9283  elfzmlbp  13555  elfzo2  13578  pythagtriplem2  16745  pythagtrip  16762  xpsfrnel  17483  fucinv  17900  setcinv  18014  rngcinv  20570  ringcinv  20604  xrsdsreclb  21368  ordthaus  23328  regr1lem2  23684  xmetrtri2  24300  clmvscom  25046  hlcomb  28675  nb3grpr2  29456  nb3gr2nb  29457  rusgrnumwwlkslem  30045  ablomuldiv  30627  nvscom  30704  cnvadj  31967  iocinif  32861  fzto1st  33185  psgnfzto1st  33187  bnj312  34868  cgr3permute1  36242  lineext  36270  colinbtwnle  36312  outsideofcom  36322  linecom  36344  linerflx2  36345  cdlemg33d  40969  uunT12p3  45042  ichexmpl2  47716  grtriproplem  48185  grtrif1o  48188  rngcinvALTV  48522  ringcinvALTV  48556