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 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anrot  1099  elioore  13418  leexp2  14212  swrdswrd  14744  pcgcd  16917  ablsubadd23  19832  ablsubsub23  19843  xmetrtri  24366  phtpcer  25028  ishl2  25405  rusgrprc  29609  clwwlknon2num  30125  ablo32  30569  ablodivdiv  30573  ablodiv32  30575  bnj268  34724  bnj945  34788  bnj944  34953  bnj969  34961  loop1cycl  35143  btwncom  36016  btwnswapid2  36020  btwnouttr  36026  cgr3permute1  36050  colinearperm1  36064  endofsegid  36087  colinbtwnle  36120  broutsideof2  36124  outsideofcom  36130  neificl  37761  lhpexle2  40013  faosnf0.11b  43445  dfsucon  43541  uunTT1p1  44819  uun123  44833  smflimlem4  46794  ichexmpl1  47461  prproropf1o  47499  grtriproplem  47911  grtrif1o  47914  alsi-no-surprise  49370