Theorem 3ancomb 1086

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

Assertion

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

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1074	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1083	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
3	1, 2	bitr4i 267	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  3anrot  1087  3simpbOLD  1145  an33rean  1587  elioore  12390  leexp2  13101  swrdswrd  13652  pcgcd  15776  ablsubsub23  18422  xmetrtri  22353  phtpcer  22987  ishl2  23358  rusgrprc  26688  clwwlknon2num  27245  ablo32  27704  ablodivdiv  27708  ablodiv32  27710  bnj268  31076  bnj945  31143  bnj944  31307  bnj969  31315  btwncom  32419  btwnswapid2  32423  btwnouttr  32429  cgr3permute1  32453  colinearperm1  32467  endofsegid  32490  colinbtwnle  32523  broutsideof2  32527  outsideofcom  32533  neificl  33854  lhpexle2  35791  uunTT1p1  39515  uun123  39529  smflimlem4  41480  alsi-no-surprise  43047