Theorem 3ancomb 1099

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

Assertion

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

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1089	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1097	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
3	1, 2	bitr4i 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anrot  1100  elioore  13328  leexp2  14133  swrdswrd  14667  pcgcd  16849  ablsubadd23  19788  ablsubsub23  19799  xmetrtri  24320  phtpcer  24962  ishl2  25337  rusgrprc  29659  clwwlknon2num  30175  ablo32  30620  ablodivdiv  30624  ablodiv32  30626  bnj268  34852  bnj945  34916  bnj944  35080  bnj969  35088  loop1cycl  35319  btwncom  36196  btwnswapid2  36200  btwnouttr  36206  cgr3permute1  36230  colinearperm1  36244  endofsegid  36267  colinbtwnle  36300  broutsideof2  36304  outsideofcom  36310  neificl  38074  lhpexle2  40456  faosnf0.11b  43854  dfsucon  43950  uunTT1p1  45220  uun123  45234  smflimlem4  47202  ichexmpl1  47929  prproropf1o  47967  grtriproplem  48415  grtrif1o  48418  alsi-no-surprise  50271