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  19727  ablsubsub23  19738  xmetrtri  24276  phtpcer  24927  ishl2  25303  rusgrprc  29571  clwwlknon2num  30084  ablo32  30528  ablodivdiv  30532  ablodiv32  30534  bnj268  34692  bnj945  34756  bnj944  34921  bnj969  34929  loop1cycl  35117  btwncom  35995  btwnswapid2  35999  btwnouttr  36005  cgr3permute1  36029  colinearperm1  36043  endofsegid  36066  colinbtwnle  36099  broutsideof2  36103  outsideofcom  36109  neificl  37740  lhpexle2  39997  faosnf0.11b  43409  dfsucon  43505  uunTT1p1  44776  uun123  44790  smflimlem4  46765  ichexmpl1  47463  prproropf1o  47501  grtriproplem  47931  grtrif1o  47934  alsi-no-surprise  49778