Theorem 3ancomb 1096

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

Assertion

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

Proof of Theorem 3ancomb

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

Syntax hints:   ↔ wb 205   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  3anrot  1097  elioore  13408  leexp2  14190  swrdswrd  14713  pcgcd  16880  ablsubadd23  19811  ablsubsub23  19822  xmetrtri  24352  phtpcer  25012  ishl2  25389  rusgrprc  29527  clwwlknon2num  30038  ablo32  30482  ablodivdiv  30486  ablodiv32  30488  bnj268  34554  bnj945  34618  bnj944  34783  bnj969  34791  loop1cycl  34965  btwncom  35838  btwnswapid2  35842  btwnouttr  35848  cgr3permute1  35872  colinearperm1  35886  endofsegid  35909  colinbtwnle  35942  broutsideof2  35946  outsideofcom  35952  neificl  37454  lhpexle2  39709  faosnf0.11b  43094  dfsucon  43190  uunTT1p1  44470  uun123  44484  smflimlem4  46395  ichexmpl1  47041  prproropf1o  47079  alsi-no-surprise  48544