Theorem 3anan12 1112

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

Assertion

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

Proof of Theorem 3anan12

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anan32  1113  3ancoma  1115  an33rean  1514  2reu5lem3  3717  snopeqop  5481  dff1o2  6838  ixxun  13502  elfz1b  13737  mreexexlem4d  17833  unocv  21998  iunocv  21999  iscvsp  25461  mbfmax  25982  ulm2  26724  iswwlks  30437  wwlksnfi  30507  eclclwwlkn1  30678  clwwlknon2x  30706  bnj548  35580  pridlnr  39110  brres2  39345  xrninxp  39487  sineq0ALT  46058  elbigo  49802