Theorem 3ancomb 1100

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

Assertion

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

Proof of Theorem 3ancomb

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3anrot  1101  an33reanOLD  1485  elioore  13350  leexp2  14132  swrdswrd  14651  pcgcd  16807  ablsubadd23  19673  ablsubsub23  19684  xmetrtri  23843  phtpcer  24493  ishl2  24869  rusgrprc  28827  clwwlknon2num  29338  ablo32  29780  ablodivdiv  29784  ablodiv32  29786  bnj268  33658  bnj945  33722  bnj944  33887  bnj969  33895  loop1cycl  34066  btwncom  34924  btwnswapid2  34928  btwnouttr  34934  cgr3permute1  34958  colinearperm1  34972  endofsegid  34995  colinbtwnle  35028  broutsideof2  35032  outsideofcom  35038  neificl  36559  lhpexle2  38819  faosnf0.11b  42111  dfsucon  42207  uunTT1p1  43488  uun123  43502  smflimlem4  45425  ichexmpl1  46072  prproropf1o  46110  alsi-no-surprise  47745