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  13289  leexp2  14092  swrdswrd  14626  pcgcd  16804  ablsubadd23  19740  ablsubsub23  19751  xmetrtri  24297  phtpcer  24948  ishl2  25324  rusgrprc  29613  clwwlknon2num  30129  ablo32  30573  ablodivdiv  30577  ablodiv32  30579  bnj268  34814  bnj945  34878  bnj944  35043  bnj969  35051  loop1cycl  35280  btwncom  36157  btwnswapid2  36161  btwnouttr  36167  cgr3permute1  36191  colinearperm1  36205  endofsegid  36228  colinbtwnle  36261  broutsideof2  36265  outsideofcom  36271  neificl  37893  lhpexle2  40209  faosnf0.11b  43610  dfsucon  43706  uunTT1p1  44976  uun123  44990  smflimlem4  46960  ichexmpl1  47657  prproropf1o  47695  grtriproplem  48127  grtrif1o  48130  alsi-no-surprise  49983