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  38688  lhpexle2  41068  faosnf0.11b  44428  dfsucon  44524  uunTT1p1  45776  uun123  45790  smflimlem4  47784  ichexmpl1  48551  prproropf1o  48589  grtriproplem  49037  grtrif1o  49040  als-no-surprise  50902