Theorem 3anan12 1110

Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised to shorten 3ancoma 1113 by Wolf Lammen, 5-Jun-2022.)

Assertion

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

Proof of Theorem 3anan12

Step	Hyp	Ref	Expression
1		3anass 1109	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12 657	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3anan32  1111  3ancoma  1113  an33rean  1511  2reu5lem3  3729  snopeqop  5490  dff1o2  6827  ixxun  13388  elfz1b  13621  mreexexlem4d  17703  unocv  21799  iunocv  21800  iscvsp  25256  mbfmax  25777  ulm2  26514  iswwlks  30126  wwlksnfi  30196  eclclwwlkn1  30367  clwwlknon2x  30395  bnj548  35230  pridlnr  38575  brres2  38812  xrninxp  38954  sineq0ALT  45537  elbigo  49216