Theorem 3ancomb 1114

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

Assertion

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

Proof of Theorem 3ancomb

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  3anrot  1115  elioore  13402  leexp2  14207  swrdswrd  14742  pcgcd  16938  ablsubadd23  19883  ablsubsub23  19894  xmetrtri  24481  phtpcer  25123  ishl2  25498  rusgrprc  29881  clwwlknon2num  30397  ablo32  30842  ablodivdiv  30846  ablodiv32  30848  bnj268  35043  bnj945  35107  bnj944  35271  bnj969  35279  loop1cycl  35528  btwncom  36405  btwnswapid2  36409  btwnouttr  36415  cgr3permute1  36439  colinearperm1  36453  endofsegid  36476  colinbtwnle  36509  broutsideof2  36513  outsideofcom  36519  neificl  38292  lhpexle2  40674  faosnf0.11b  44045  dfsucon  44141  uunTT1p1  45394  uun123  45408  smflimlem4  47380  ichexmpl1  48107  prproropf1o  48145  grtriproplem  48593  grtrif1o  48596  als-no-surprise  50469