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  13414  leexp2  14208  swrdswrd  14740  pcgcd  16912  ablsubadd23  19846  ablsubsub23  19857  xmetrtri  24381  phtpcer  25041  ishl2  25418  rusgrprc  29623  clwwlknon2num  30134  ablo32  30578  ablodivdiv  30582  ablodiv32  30584  bnj268  34702  bnj945  34766  bnj944  34931  bnj969  34939  loop1cycl  35122  btwncom  35996  btwnswapid2  36000  btwnouttr  36006  cgr3permute1  36030  colinearperm1  36044  endofsegid  36067  colinbtwnle  36100  broutsideof2  36104  outsideofcom  36110  neificl  37740  lhpexle2  39993  faosnf0.11b  43417  dfsucon  43513  uunTT1p1  44792  uun123  44806  smflimlem4  46730  ichexmpl1  47394  prproropf1o  47432  grtriproplem  47844  grtrif1o  47847  alsi-no-surprise  49027