Theorem 3ancomb 1098

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

Assertion

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

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1088	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1096	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
3	1, 2	bitr4i 277	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3anrot  1099  an33reanOLD  1483  elioore  13109  leexp2  13889  swrdswrd  14418  pcgcd  16579  ablsubsub23  19426  xmetrtri  23508  phtpcer  24158  ishl2  24534  rusgrprc  27957  clwwlknon2num  28469  ablo32  28911  ablodivdiv  28915  ablodiv32  28917  bnj268  32688  bnj945  32753  bnj944  32918  bnj969  32926  loop1cycl  33099  btwncom  34316  btwnswapid2  34320  btwnouttr  34326  cgr3permute1  34350  colinearperm1  34364  endofsegid  34387  colinbtwnle  34420  broutsideof2  34424  outsideofcom  34430  neificl  35911  lhpexle2  38024  dfsucon  41130  uunTT1p1  42414  uun123  42428  smflimlem4  44309  ichexmpl1  44921  prproropf1o  44959  alsi-no-surprise  46500