Theorem 3ancoma 1094

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3anrot  1096  3anrev  1097  cadcomb  1610  f13dfv  7025  suppssfifsupp  8842  elfzmlbp  13012  elfzo2  13035  pythagtriplem2  16148  pythagtrip  16165  xpsfrnel  16829  fucinv  17237  setcinv  17344  xrsdsreclb  20586  ordthaus  21986  regr1lem2  22342  xmetrtri2  22960  clmvscom  23688  hlcomb  26383  nb3grpr2  27159  nb3gr2nb  27160  rusgrnumwwlkslem  27742  ablomuldiv  28323  nvscom  28400  cnvadj  29663  iocinif  30498  fzto1st  30740  psgnfzto1st  30742  bnj312  31977  cgr3permute1  33504  lineext  33532  colinbtwnle  33574  outsideofcom  33584  linecom  33606  linerflx2  33607  cdlemg33d  37839  uunT12p3  41129  ichexmpl2  43626  rngcinv  44246  rngcinvALTV  44258  ringcinv  44297  ringcinvALTV  44321