Theorem 3ancomb 1096

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

Assertion

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

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1086	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1094	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
3	1, 2	bitr4i 281	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3anrot  1097  an33reanOLD  1481  elioore  12756  leexp2  13531  swrdswrd  14058  pcgcd  16204  ablsubsub23  18938  xmetrtri  22962  phtpcer  23600  ishl2  23974  rusgrprc  27380  clwwlknon2num  27890  ablo32  28332  ablodivdiv  28336  ablodiv32  28338  bnj268  32089  bnj945  32155  bnj944  32320  bnj969  32328  loop1cycl  32497  btwncom  33588  btwnswapid2  33592  btwnouttr  33598  cgr3permute1  33622  colinearperm1  33636  endofsegid  33659  colinbtwnle  33692  broutsideof2  33696  outsideofcom  33702  neificl  35191  lhpexle2  37306  dfsucon  40231  uunTT1p1  41500  uun123  41514  smflimlem4  43407  ichexmpl1  43986  prproropf1o  44024  alsi-no-surprise  45324