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  13303  leexp2  14106  swrdswrd  14640  pcgcd  16818  ablsubadd23  19754  ablsubsub23  19765  xmetrtri  24311  phtpcer  24962  ishl2  25338  rusgrprc  29676  clwwlknon2num  30192  ablo32  30637  ablodivdiv  30641  ablodiv32  30643  bnj268  34886  bnj945  34950  bnj944  35114  bnj969  35122  loop1cycl  35353  btwncom  36230  btwnswapid2  36234  btwnouttr  36240  cgr3permute1  36264  colinearperm1  36278  endofsegid  36301  colinbtwnle  36334  broutsideof2  36338  outsideofcom  36344  neificl  38004  lhpexle2  40386  faosnf0.11b  43783  dfsucon  43879  uunTT1p1  45149  uun123  45163  smflimlem4  47132  ichexmpl1  47829  prproropf1o  47867  grtriproplem  48299  grtrif1o  48302  alsi-no-surprise  50155