Theorem 3ancoma 1115

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anrot  1117  3anrev  1118  cadcomb  1645  f13dfv  7283  suppssfifsupp  9376  elfzmlbp  13777  elfzo2  13800  pythagtriplem2  17001  pythagtrip  17018  xpsfrnel  17740  fucinv  18157  setcinv  18271  rngcinv  20895  ringcinv  20929  xrsdsreclb  21726  ordthaus  23708  regr1lem2  24065  xmetrtri2  24681  clmvscom  25417  hlcomb  29075  nb3grpr2  29970  nb3gr2nb  29971  rusgrnumwwlkslem  30567  ablomuldiv  31160  nvscom  31237  cnvadj  32500  iocinif  33420  fzto1st  33711  psgnfzto1st  33713  bnj312  35390  cgr3permute1  36906  lineext  36934  colinbtwnle  36976  outsideofcom  36986  linecom  37008  linerflx2  37009  cdlemg33d  41860  uunT12p3  45878  ichexmpl2  48646  grtriproplem  49131  grtrif1o  49134  rngcinvALTV  49467  ringcinvALTV  49501