Theorem 3anan12 1095

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

Assertion

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

Proof of Theorem 3anan12

Step	Hyp	Ref	Expression
1		3anass 1094	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12 645	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitri 275	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:  3ancoma  1097  an33rean  1485  2reu5lem3  3728  snopeqop  5466  dff1o2  6805  ixxun  13322  elfz1b  13554  mreexexlem4d  17608  unocv  21589  iunocv  21590  iscvsp  25028  mbfmax  25550  ulm2  26294  iswwlks  29766  wwlksnfi  29836  eclclwwlkn1  30004  clwwlknon2x  30032  bnj548  34887  pridlnr  38030  brres2  38257  xrninxp  38378  sineq0ALT  44926  elbigo  48537