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  13397  leexp2  14194  swrdswrd  14728  pcgcd  16903  ablsubadd23  19799  ablsubsub23  19810  xmetrtri  24299  phtpcer  24950  ishl2  25327  rusgrprc  29575  clwwlknon2num  30091  ablo32  30535  ablodivdiv  30539  ablodiv32  30541  bnj268  34745  bnj945  34809  bnj944  34974  bnj969  34982  loop1cycl  35164  btwncom  36037  btwnswapid2  36041  btwnouttr  36047  cgr3permute1  36071  colinearperm1  36085  endofsegid  36108  colinbtwnle  36141  broutsideof2  36145  outsideofcom  36151  neificl  37782  lhpexle2  40034  faosnf0.11b  43426  dfsucon  43522  uunTT1p1  44793  uun123  44807  smflimlem4  46783  ichexmpl1  47463  prproropf1o  47501  grtriproplem  47931  grtrif1o  47934  alsi-no-surprise  49640