Theorem 3ancomb 1122

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

Assertion

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

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1110	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1119	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
3	1, 2	bitr4i 270	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 198   ∧ wa 385   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  3anrot  1123  3simpbOLD  1182  an33rean  1608  elioore  12450  leexp2  13165  swrdswrd  13744  pcgcd  15911  ablsubsub23  18541  xmetrtri  22484  phtpcer  23118  ishl2  23492  rusgrprc  26831  clwwlknon2num  27435  ablo32  27920  ablodivdiv  27924  ablodiv32  27926  bnj268  31286  bnj945  31352  bnj944  31516  bnj969  31524  btwncom  32625  btwnswapid2  32629  btwnouttr  32635  cgr3permute1  32659  colinearperm1  32673  endofsegid  32696  colinbtwnle  32729  broutsideof2  32733  outsideofcom  32739  neificl  34027  lhpexle2  36022  uunTT1p1  39777  uun123  39791  smflimlem4  41715  alsi-no-surprise  43331