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  13513  leexp2  14321  swrdswrd  14862  pcgcd  17065  ablsubadd23  20036  ablsubsub23  20047  xmetrtri  24683  phtpcer  25325  ishl2  25700  rusgrprc  30180  clwwlknon2num  30705  loop1cycl  30753  ablo32  31160  ablodivdiv  31164  ablodiv32  31166  bnj268  35390  bnj945  35454  bnj944  35618  bnj969  35626  btwncom  36903  btwnswapid2  36907  btwnouttr  36913  cgr3permute1  36937  colinearperm1  36951  endofsegid  36974  colinbtwnle  37007  broutsideof2  37011  outsideofcom  37017  neificl  38824  lhpexle2  41204  faosnf0.11b  44565  dfsucon  44661  uunTT1p1  45912  uun123  45926  smflimlem4  47920  ichexmpl1  48687  prproropf1o  48725  grtriproplem  49173  grtrif1o  49176  als-no-surprise  51113