Theorem 3ancomb 1111

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

Assertion

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

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1100	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1108	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
3	1, 2	bitr4i 280	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  3anrot  1112  elioore  13379  leexp2  14184  swrdswrd  14718  pcgcd  16914  ablsubadd23  19853  ablsubsub23  19864  xmetrtri  24415  phtpcer  25057  ishl2  25432  rusgrprc  29791  clwwlknon2num  30307  ablo32  30752  ablodivdiv  30756  ablodiv32  30758  bnj268  35005  bnj945  35069  bnj944  35233  bnj969  35241  loop1cycl  35487  btwncom  36364  btwnswapid2  36368  btwnouttr  36374  cgr3permute1  36398  colinearperm1  36412  endofsegid  36435  colinbtwnle  36468  broutsideof2  36472  outsideofcom  36478  neificl  38252  lhpexle2  40634  faosnf0.11b  44003  dfsucon  44099  uunTT1p1  45369  uun123  45383  smflimlem4  47348  ichexmpl1  48075  prproropf1o  48113  grtriproplem  48561  grtrif1o  48564  alsi-no-surprise  50417