Theorem 3ancomb 1116

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

Assertion

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

Proof of Theorem 3ancomb

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anrot  1117  elioore  13506  leexp2  14314  swrdswrd  14854  pcgcd  17056  ablsubadd23  20027  ablsubsub23  20038  xmetrtri  24674  phtpcer  25316  ishl2  25691  rusgrprc  30171  clwwlknon2num  30696  loop1cycl  30744  ablo32  31151  ablodivdiv  31155  ablodiv32  31157  bnj268  35340  bnj945  35404  bnj944  35568  bnj969  35576  btwncom  36779  btwnswapid2  36783  btwnouttr  36789  cgr3permute1  36813  colinearperm1  36827  endofsegid  36850  colinbtwnle  36883  broutsideof2  36887  outsideofcom  36893  neificl  38687  lhpexle2  41067  faosnf0.11b  44427  dfsucon  44523  uunTT1p1  45775  uun123  45789  smflimlem4  47783  ichexmpl1  48550  prproropf1o  48588  grtriproplem  49036  grtrif1o  49039  als-no-surprise  50901