Theorem 3anan12 1092

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

Assertion

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

Proof of Theorem 3anan12

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3ancoma  1094  an33rean  1479  an33reanOLD  1480  2reu5lem3  3748  snopeqop  5396  dff1o2  6620  ixxun  12755  elfz1b  12977  mreexexlem4d  16918  unocv  20824  iunocv  20825  iscvsp  23732  mbfmax  24250  ulm2  24973  iswwlks  27614  wwlksnfi  27684  wwlksnfiOLD  27685  eclclwwlkn1  27854  clwwlknon2x  27882  bnj548  32169  pridlnr  35329  brres2  35544  xrninxp  35655  sineq0ALT  41291  elbigo  44631