Theorem 3ancomb 1098

Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Revised to shorten 3anrot 1099 by Wolf Lammen, 9-Jun-2022.)

Assertion

Ref	Expression
3ancomb	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1088	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1096	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
3	1, 2	bitr4i 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

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

This theorem is referenced by:  3anrot  1099  elioore  13275  leexp2  14078  swrdswrd  14612  pcgcd  16790  ablsubadd23  19725  ablsubsub23  19736  xmetrtri  24270  phtpcer  24921  ishl2  25297  rusgrprc  29569  clwwlknon2num  30085  ablo32  30529  ablodivdiv  30533  ablodiv32  30535  bnj268  34721  bnj945  34785  bnj944  34950  bnj969  34958  loop1cycl  35181  btwncom  36058  btwnswapid2  36062  btwnouttr  36068  cgr3permute1  36092  colinearperm1  36106  endofsegid  36129  colinbtwnle  36162  broutsideof2  36166  outsideofcom  36172  neificl  37803  lhpexle2  40119  faosnf0.11b  43530  dfsucon  43626  uunTT1p1  44896  uun123  44910  smflimlem4  46882  ichexmpl1  47579  prproropf1o  47617  grtriproplem  48049  grtrif1o  48052  alsi-no-surprise  49907