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  13336  leexp2  14136  swrdswrd  14670  pcgcd  16849  ablsubadd23  19743  ablsubsub23  19754  xmetrtri  24243  phtpcer  24894  ishl2  25270  rusgrprc  29518  clwwlknon2num  30034  ablo32  30478  ablodivdiv  30482  ablodiv32  30484  bnj268  34699  bnj945  34763  bnj944  34928  bnj969  34936  loop1cycl  35124  btwncom  36002  btwnswapid2  36006  btwnouttr  36012  cgr3permute1  36036  colinearperm1  36050  endofsegid  36073  colinbtwnle  36106  broutsideof2  36110  outsideofcom  36116  neificl  37747  lhpexle2  40004  faosnf0.11b  43416  dfsucon  43512  uunTT1p1  44783  uun123  44797  smflimlem4  46772  ichexmpl1  47470  prproropf1o  47508  grtriproplem  47938  grtrif1o  47941  alsi-no-surprise  49785