Theorem 3ancomb 1099

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

Assertion

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

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1089	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1097	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
3	1, 2	bitr4i 277	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3anrot  1100  an33reanOLD  1484  elioore  13358  leexp2  14140  swrdswrd  14659  pcgcd  16815  ablsubadd23  19722  ablsubsub23  19733  xmetrtri  24081  phtpcer  24735  ishl2  25111  rusgrprc  29102  clwwlknon2num  29613  ablo32  30057  ablodivdiv  30061  ablodiv32  30063  bnj268  34006  bnj945  34070  bnj944  34235  bnj969  34243  loop1cycl  34414  btwncom  35278  btwnswapid2  35282  btwnouttr  35288  cgr3permute1  35312  colinearperm1  35326  endofsegid  35349  colinbtwnle  35382  broutsideof2  35386  outsideofcom  35392  neificl  36924  lhpexle2  39184  faosnf0.11b  42480  dfsucon  42576  uunTT1p1  43857  uun123  43871  smflimlem4  45789  ichexmpl1  46436  prproropf1o  46474  alsi-no-surprise  47931