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  3725  snopeqop  5461  dff1o2  6787  ixxun  13298  elfz1b  13530  mreexexlem4d  17584  unocv  21565  iunocv  21566  iscvsp  25004  mbfmax  25526  ulm2  26270  iswwlks  29739  wwlksnfi  29809  eclclwwlkn1  29977  clwwlknon2x  30005  bnj548  34860  pridlnr  38003  brres2  38230  xrninxp  38351  sineq0ALT  44899  elbigo  48513