Theorem 3ancomb 1098

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

Assertion

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

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		df-3an 1088	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3anan32 1096	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
3	1, 2	bitr4i 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anrot  1099  elioore  13312  leexp2  14112  swrdswrd  14646  pcgcd  16825  ablsubadd23  19719  ablsubsub23  19730  xmetrtri  24219  phtpcer  24870  ishl2  25246  rusgrprc  29494  clwwlknon2num  30007  ablo32  30451  ablodivdiv  30455  ablodiv32  30457  bnj268  34672  bnj945  34736  bnj944  34901  bnj969  34909  loop1cycl  35097  btwncom  35975  btwnswapid2  35979  btwnouttr  35985  cgr3permute1  36009  colinearperm1  36023  endofsegid  36046  colinbtwnle  36079  broutsideof2  36083  outsideofcom  36089  neificl  37720  lhpexle2  39977  faosnf0.11b  43389  dfsucon  43485  uunTT1p1  44756  uun123  44770  smflimlem4  46745  ichexmpl1  47443  prproropf1o  47481  grtriproplem  47911  grtrif1o  47914  alsi-no-surprise  49758