Theorem 3ancomb 1099

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

Assertion

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

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1089	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1097	. 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  elioore  13322  leexp2  14127  swrdswrd  14661  pcgcd  16843  ablsubadd23  19782  ablsubsub23  19793  xmetrtri  24333  phtpcer  24975  ishl2  25350  rusgrprc  29677  clwwlknon2num  30193  ablo32  30638  ablodivdiv  30642  ablodiv32  30644  bnj268  34871  bnj945  34935  bnj944  35099  bnj969  35107  loop1cycl  35338  btwncom  36215  btwnswapid2  36219  btwnouttr  36225  cgr3permute1  36249  colinearperm1  36263  endofsegid  36286  colinbtwnle  36319  broutsideof2  36323  outsideofcom  36329  neificl  38091  lhpexle2  40473  faosnf0.11b  43875  dfsucon  43971  uunTT1p1  45241  uun123  45255  smflimlem4  47223  ichexmpl1  47944  prproropf1o  47982  grtriproplem  48430  grtrif1o  48433  alsi-no-surprise  50286