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 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

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

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 1105

This theorem is referenced by:  3anrot  1117  elioore  13397  leexp2  14203  swrdswrd  14738  pcgcd  16933  ablsubadd23  19878  ablsubsub23  19889  xmetrtri  24512  phtpcer  25154  ishl2  25529  rusgrprc  29940  clwwlknon2num  30456  ablo32  30901  ablodivdiv  30905  ablodiv32  30907  bnj268  35098  bnj945  35162  bnj944  35326  bnj969  35334  loop1cycl  35629  btwncom  36506  btwnswapid2  36510  btwnouttr  36516  cgr3permute1  36540  colinearperm1  36554  endofsegid  36577  colinbtwnle  36610  broutsideof2  36614  outsideofcom  36620  neificl  38424  lhpexle2  40804  faosnf0.11b  44173  dfsucon  44269  uunTT1p1  45522  uun123  45536  smflimlem4  47508  ichexmpl1  48238  prproropf1o  48276  grtriproplem  48724  grtrif1o  48727  als-no-surprise  50604