Theorem 3anan32 1113

Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Shortened by Garrett Katz, 15-Jun-2026.)

Assertion

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

Proof of Theorem 3anan32

Step	Hyp	Ref	Expression
1		3anan12 1112	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2	1	biancomi 468	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:  3ancomb  1116  anandi3r  1120  rabssrabd  4038  dff1o3  6831  bropfvvvvlem  8092  tz7.49c  8439  ispos2  18395  lbsacsbs  21332  obslbs  21932  islbs4  22034  leordtvallem1  23419  trfbas2  24053  isclmp  25309  lssbn  25564  sineq0  26742  dchrelbas3  27455  elno3  27872  nb3grpr2  29793  uspgr2wlkeq  30055  2spthd  30359  clwwlknonwwlknonb  30526  frgr2wwlkeu  30751  elicoelioo  33195  cndprobprob  34895  bnj543  35348  cusgr3cyclex  35671  ellimits  36439  eldmxrncnvepres  39143  eldmxrncnvepres2  39144  refsymrel2  39360  refsymrel3  39361  dfeqvrel2  39383  dfeqvrel3  39384  i0oii  49757