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  13278  leexp2  14078  swrdswrd  14611  pcgcd  16790  ablsubadd23  19692  ablsubsub23  19703  xmetrtri  24241  phtpcer  24892  ishl2  25268  rusgrprc  29536  clwwlknon2num  30049  ablo32  30493  ablodivdiv  30497  ablodiv32  30499  bnj268  34676  bnj945  34740  bnj944  34905  bnj969  34913  loop1cycl  35114  btwncom  35992  btwnswapid2  35996  btwnouttr  36002  cgr3permute1  36026  colinearperm1  36040  endofsegid  36063  colinbtwnle  36096  broutsideof2  36100  outsideofcom  36106  neificl  37737  lhpexle2  39993  faosnf0.11b  43404  dfsucon  43500  uunTT1p1  44771  uun123  44785  smflimlem4  46759  ichexmpl1  47457  prproropf1o  47495  grtriproplem  47927  grtrif1o  47930  alsi-no-surprise  49785