Theorem 3ancomb 1100

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

Assertion

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

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1090	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1098	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
3	1, 2	bitr4i 281	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  3anrot  1101  an33reanOLD  1485  elioore  12844  leexp2  13620  swrdswrd  14149  pcgcd  16307  ablsubsub23  19057  xmetrtri  23101  phtpcer  23740  ishl2  24115  rusgrprc  27524  clwwlknon2num  28034  ablo32  28476  ablodivdiv  28480  ablodiv32  28482  bnj268  32250  bnj945  32316  bnj944  32481  bnj969  32489  loop1cycl  32662  btwncom  33946  btwnswapid2  33950  btwnouttr  33956  cgr3permute1  33980  colinearperm1  33994  endofsegid  34017  colinbtwnle  34050  broutsideof2  34054  outsideofcom  34060  neificl  35523  lhpexle2  37636  dfsucon  40668  uunTT1p1  41936  uun123  41950  smflimlem4  43832  ichexmpl1  44439  prproropf1o  44477  alsi-no-surprise  45937