Theorem 3ancomb 1095

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

Assertion

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

Proof of Theorem 3ancomb

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3anrot  1096  an33reanOLD  1480  elioore  12769  leexp2  13536  swrdswrd  14067  pcgcd  16214  ablsubsub23  18945  xmetrtri  22965  phtpcer  23599  ishl2  23973  rusgrprc  27372  clwwlknon2num  27884  ablo32  28326  ablodivdiv  28330  ablodiv32  28332  bnj268  31979  bnj945  32045  bnj944  32210  bnj969  32218  loop1cycl  32384  btwncom  33475  btwnswapid2  33479  btwnouttr  33485  cgr3permute1  33509  colinearperm1  33523  endofsegid  33546  colinbtwnle  33579  broutsideof2  33583  outsideofcom  33589  neificl  35043  lhpexle2  37161  dfsucon  39909  uunTT1p1  41148  uun123  41162  smflimlem4  43070  ichexmpl1  43651  prproropf1o  43689  alsi-no-surprise  44917