Theorem 3anan12 1044

Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)

Assertion

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

Proof of Theorem 3anan12

Step	Hyp	Ref	Expression
1		3ancoma 1038	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3anass 1035	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitri 263	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  an33rean  1438  2reu5lem3  3382  snopeqop  4894  fncnv  5876  dff1o2  6055  ixxun  12062  mreexexlem4d  16130  unocv  19843  iunocv  19844  iscvsp  22736  mbfmax  23222  ulm2  23943  usgra2wlkspthlem2  26148  wwlknprop  26214  wwlknfi  26266  eclclwwlkn1  26359  numclwwlkovf2  26611  numclwlk1lem2f1  26621  bnj548  30221  pridlnr  33005  sineq0ALT  38195  iswwlks  41039  wwlksnfi  41112  eclclwwlksn1  41259  av-numclwlk1lem2f1  41524  elbigo  42143