Theorem 3anan12 1107

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 1110 by Wolf Lammen, 5-Jun-2022.)

Assertion

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

Proof of Theorem 3anan12

Step	Hyp	Ref	Expression
1		3anass 1106	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12 655	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitri 277	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 208   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  3anan32  1108  3ancoma  1110  an33rean  1504  2reu5lem3  3720  snopeqop  5475  dff1o2  6812  ixxun  13365  elfz1b  13598  mreexexlem4d  17679  unocv  21732  iunocv  21733  iscvsp  25190  mbfmax  25711  ulm2  26448  iswwlks  30036  wwlksnfi  30106  eclclwwlkn1  30277  clwwlknon2x  30305  bnj548  35192  pridlnr  38535  brres2  38772  xrninxp  38914  sineq0ALT  45512  elbigo  49173