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 277	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3anrot  1099  3anrev  1100  cadcomb  1613  f13dfv  7202  suppssfifsupp  9241  elfzmlbp  13468  elfzo2  13491  pythagtriplem2  16615  pythagtrip  16632  xpsfrnel  17370  fucinv  17788  setcinv  17902  xrsdsreclb  20751  ordthaus  22641  regr1lem2  22997  xmetrtri2  23615  clmvscom  24359  hlcomb  27253  nb3grpr2  28039  nb3gr2nb  28040  rusgrnumwwlkslem  28622  ablomuldiv  29202  nvscom  29279  cnvadj  30542  iocinif  31389  fzto1st  31657  psgnfzto1st  31659  bnj312  32991  cgr3permute1  34446  lineext  34474  colinbtwnle  34516  outsideofcom  34526  linecom  34548  linerflx2  34549  cdlemg33d  38985  uunT12p3  42751  ichexmpl2  45281  rngcinv  45898  rngcinvALTV  45910  ringcinv  45949  ringcinvALTV  45973