Theorem 3ancomb 1097

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

Assertion

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

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1087	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1095	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
3	1, 2	bitr4i 277	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  3anrot  1098  an33reanOLD  1482  elioore  13038  leexp2  13817  swrdswrd  14346  pcgcd  16507  ablsubsub23  19341  xmetrtri  23416  phtpcer  24064  ishl2  24439  rusgrprc  27860  clwwlknon2num  28370  ablo32  28812  ablodivdiv  28816  ablodiv32  28818  bnj268  32588  bnj945  32653  bnj944  32818  bnj969  32826  loop1cycl  32999  btwncom  34243  btwnswapid2  34247  btwnouttr  34253  cgr3permute1  34277  colinearperm1  34291  endofsegid  34314  colinbtwnle  34347  broutsideof2  34351  outsideofcom  34357  neificl  35838  lhpexle2  37951  dfsucon  41028  uunTT1p1  42303  uun123  42317  smflimlem4  44196  ichexmpl1  44809  prproropf1o  44847  alsi-no-surprise  46386