Theorem 3ancomb 1116

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

Assertion

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

Proof of Theorem 3ancomb

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anrot  1117  elioore  13429  leexp2  14236  swrdswrd  14775  pcgcd  16971  ablsubadd23  19941  ablsubsub23  19952  xmetrtri  24582  phtpcer  25224  ishl2  25599  rusgrprc  30051  clwwlknon2num  30576  loop1cycl  30624  ablo32  31031  ablodivdiv  31035  ablodiv32  31037  bnj268  35220  bnj945  35284  bnj944  35448  bnj969  35456  btwncom  36595  btwnswapid2  36599  btwnouttr  36605  cgr3permute1  36629  colinearperm1  36643  endofsegid  36666  colinbtwnle  36699  broutsideof2  36703  outsideofcom  36709  neificl  38504  lhpexle2  40884  faosnf0.11b  44268  dfsucon  44364  uunTT1p1  45617  uun123  45631  smflimlem4  47603  ichexmpl1  48370  prproropf1o  48408  grtriproplem  48856  grtrif1o  48859  als-no-surprise  50736