Theorem 3ancoma 1098

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 1096	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2		3anass 1095	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4i 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anrot  1100  3anrev  1101  cadcomb  1615  f13dfv  7222  suppssfifsupp  9286  elfzmlbp  13584  elfzo2  13607  pythagtriplem2  16779  pythagtrip  16796  xpsfrnel  17517  fucinv  17934  setcinv  18048  rngcinv  20605  ringcinv  20639  xrsdsreclb  21403  ordthaus  23359  regr1lem2  23715  xmetrtri2  24331  clmvscom  25067  hlcomb  28685  nb3grpr2  29466  nb3gr2nb  29467  rusgrnumwwlkslem  30055  ablomuldiv  30638  nvscom  30715  cnvadj  31978  iocinif  32869  fzto1st  33179  psgnfzto1st  33181  bnj312  34871  cgr3permute1  36246  lineext  36274  colinbtwnle  36316  outsideofcom  36326  linecom  36348  linerflx2  36349  cdlemg33d  41169  uunT12p3  45246  ichexmpl2  47942  grtriproplem  48427  grtrif1o  48430  rngcinvALTV  48764  ringcinvALTV  48798