Theorem 3ancoma 1095

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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3anrot  1097  3anrev  1098  cadcomb  1615  f13dfv  7009  suppssfifsupp  8832  elfzmlbp  13013  elfzo2  13036  pythagtriplem2  16144  pythagtrip  16161  xpsfrnel  16827  fucinv  17235  setcinv  17342  xrsdsreclb  20138  ordthaus  21989  regr1lem2  22345  xmetrtri2  22963  clmvscom  23695  hlcomb  26397  nb3grpr2  27173  nb3gr2nb  27174  rusgrnumwwlkslem  27755  ablomuldiv  28335  nvscom  28412  cnvadj  29675  iocinif  30530  fzto1st  30795  psgnfzto1st  30797  bnj312  32092  cgr3permute1  33622  lineext  33650  colinbtwnle  33692  outsideofcom  33702  linecom  33724  linerflx2  33725  cdlemg33d  38005  uunT12p3  41508  ichexmpl2  43987  rngcinv  44605  rngcinvALTV  44617  ringcinv  44656  ringcinvALTV  44680