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  13295  leexp2  14098  swrdswrd  14632  pcgcd  16810  ablsubadd23  19746  ablsubsub23  19757  xmetrtri  24303  phtpcer  24954  ishl2  25330  rusgrprc  29647  clwwlknon2num  30163  ablo32  30607  ablodivdiv  30611  ablodiv32  30613  bnj268  34846  bnj945  34910  bnj944  35075  bnj969  35083  loop1cycl  35312  btwncom  36189  btwnswapid2  36193  btwnouttr  36199  cgr3permute1  36223  colinearperm1  36237  endofsegid  36260  colinbtwnle  36293  broutsideof2  36297  outsideofcom  36303  neificl  37925  lhpexle2  40307  faosnf0.11b  43704  dfsucon  43800  uunTT1p1  45070  uun123  45084  smflimlem4  47054  ichexmpl1  47751  prproropf1o  47789  grtriproplem  48221  grtrif1o  48224  alsi-no-surprise  50077