Theorem 3ancomb 1104

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

Assertion

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

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1094	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1102	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
3	1, 2	bitr4i 279	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3anrot  1105  elioore  13319  leexp2  14124  swrdswrd  14658  pcgcd  16840  ablsubadd23  19779  ablsubsub23  19790  xmetrtri  24338  phtpcer  24980  ishl2  25355  rusgrprc  29677  clwwlknon2num  30193  ablo32  30638  ablodivdiv  30642  ablodiv32  30644  bnj268  34892  bnj945  34956  bnj944  35120  bnj969  35128  loop1cycl  35365  btwncom  36242  btwnswapid2  36246  btwnouttr  36252  cgr3permute1  36276  colinearperm1  36290  endofsegid  36313  colinbtwnle  36346  broutsideof2  36350  outsideofcom  36356  neificl  38120  lhpexle2  40502  faosnf0.11b  43871  dfsucon  43967  uunTT1p1  45237  uun123  45251  smflimlem4  47217  ichexmpl1  47944  prproropf1o  47982  grtriproplem  48430  grtrif1o  48433  alsi-no-surprise  50286