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  13420  leexp2  14227  swrdswrd  14766  pcgcd  16962  ablsubadd23  19929  ablsubsub23  19940  xmetrtri  24565  phtpcer  25207  ishl2  25582  rusgrprc  30000  clwwlknon2num  30525  loop1cycl  30573  ablo32  30974  ablodivdiv  30978  ablodiv32  30980  bnj268  35165  bnj945  35229  bnj944  35393  bnj969  35401  btwncom  36545  btwnswapid2  36549  btwnouttr  36555  cgr3permute1  36579  colinearperm1  36593  endofsegid  36616  colinbtwnle  36649  broutsideof2  36653  outsideofcom  36659  neificl  38464  lhpexle2  40844  faosnf0.11b  44213  dfsucon  44309  uunTT1p1  45562  uun123  45576  smflimlem4  47548  ichexmpl1  48278  prproropf1o  48316  grtriproplem  48764  grtrif1o  48767  als-no-surprise  50643