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  1615  f13dfv  7146  suppssfifsupp  9143  elfzmlbp  13367  elfzo2  13390  pythagtriplem2  16518  pythagtrip  16535  xpsfrnel  17273  fucinv  17691  setcinv  17805  xrsdsreclb  20645  ordthaus  22535  regr1lem2  22891  xmetrtri2  23509  clmvscom  24253  hlcomb  26964  nb3grpr2  27750  nb3gr2nb  27751  rusgrnumwwlkslem  28334  ablomuldiv  28914  nvscom  28991  cnvadj  30254  iocinif  31102  fzto1st  31370  psgnfzto1st  31372  bnj312  32691  cgr3permute1  34350  lineext  34378  colinbtwnle  34420  outsideofcom  34430  linecom  34452  linerflx2  34453  cdlemg33d  38723  uunT12p3  42422  ichexmpl2  44922  rngcinv  45539  rngcinvALTV  45551  ringcinv  45590  ringcinvALTV  45614