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  13291  leexp2  14094  swrdswrd  14628  pcgcd  16806  ablsubadd23  19742  ablsubsub23  19753  xmetrtri  24299  phtpcer  24950  ishl2  25326  rusgrprc  29664  clwwlknon2num  30180  ablo32  30624  ablodivdiv  30628  ablodiv32  30630  bnj268  34865  bnj945  34929  bnj944  35094  bnj969  35102  loop1cycl  35331  btwncom  36208  btwnswapid2  36212  btwnouttr  36218  cgr3permute1  36242  colinearperm1  36256  endofsegid  36279  colinbtwnle  36312  broutsideof2  36316  outsideofcom  36322  neificl  37954  lhpexle2  40280  faosnf0.11b  43678  dfsucon  43774  uunTT1p1  45044  uun123  45058  smflimlem4  47028  ichexmpl1  47725  prproropf1o  47763  grtriproplem  48195  grtrif1o  48198  alsi-no-surprise  50051