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  13437  leexp2  14221  swrdswrd  14753  pcgcd  16925  ablsubadd23  19855  ablsubsub23  19866  xmetrtri  24386  phtpcer  25046  ishl2  25423  rusgrprc  29626  clwwlknon2num  30137  ablo32  30581  ablodivdiv  30585  ablodiv32  30587  bnj268  34685  bnj945  34749  bnj944  34914  bnj969  34922  loop1cycl  35105  btwncom  35978  btwnswapid2  35982  btwnouttr  35988  cgr3permute1  36012  colinearperm1  36026  endofsegid  36049  colinbtwnle  36082  broutsideof2  36086  outsideofcom  36092  neificl  37713  lhpexle2  39967  faosnf0.11b  43389  dfsucon  43485  uunTT1p1  44765  uun123  44779  smflimlem4  46695  ichexmpl1  47343  prproropf1o  47381  grtriproplem  47790  grtrif1o  47793  alsi-no-surprise  48890