Theorem 3ancomb 1097

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

Assertion

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

Proof of Theorem 3ancomb

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

Syntax hints:   ↔ wb 205   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  3anrot  1098  an33reanOLD  1482  elioore  13358  leexp2  14140  swrdswrd  14659  pcgcd  16815  ablsubadd23  19722  ablsubsub23  19733  xmetrtri  24081  phtpcer  24741  ishl2  25118  rusgrprc  29114  clwwlknon2num  29625  ablo32  30069  ablodivdiv  30073  ablodiv32  30075  bnj268  34018  bnj945  34082  bnj944  34247  bnj969  34255  loop1cycl  34426  btwncom  35290  btwnswapid2  35294  btwnouttr  35300  cgr3permute1  35324  colinearperm1  35338  endofsegid  35361  colinbtwnle  35394  broutsideof2  35398  outsideofcom  35404  neificl  36924  lhpexle2  39184  faosnf0.11b  42480  dfsucon  42576  uunTT1p1  43857  uun123  43871  smflimlem4  45788  ichexmpl1  46435  prproropf1o  46473  alsi-no-surprise  47930