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  13546  leexp2  14354  swrdswrd  14896  pcgcd  17100  ablsubadd23  20078  ablsubsub23  20089  xmetrtri  24729  phtpcer  25371  ishl2  25746  rusgrprc  30228  clwwlknon2num  30753  loop1cycl  30801  ablo32  31208  ablodivdiv  31212  ablodiv32  31214  bnj268  35451  bnj945  35515  bnj944  35679  bnj969  35687  mirimanofffr  36670  btwncom  36994  btwnswapid2  36998  btwnouttr  37004  cgr3permute1  37028  colinearperm1  37042  endofsegid  37065  colinbtwnle  37098  broutsideof2  37102  outsideofcom  37108  neificl  38953  lhpexle2  41333  faosnf0.11b  44689  dfsucon  44785  uunTT1p1  46036  uun123  46050  smflimlem4  48057  ichexmpl1  48824  prproropf1o  48862  grtriproplem  49310  grtrif1o  49313  als-no-surprise  51330