Theorem 3anan32 1111

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 1110	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2	1	biancomi 467	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3ancomb  1114  anandi3r  1118  rabssrabd  4045  dff1o3  6828  bropfvvvvlem  8086  tz7.49c  8433  ispos2  18371  lbsacsbs  21258  obslbs  21849  islbs4  21951  leordtvallem1  23336  trfbas2  23969  isclmp  25225  lssbn  25480  sineq0  26655  dchrelbas3  27368  elno3  27785  nb3grpr2  29674  uspgr2wlkeq  29936  2spthd  30231  clwwlknonwwlknonb  30398  frgr2wwlkeu  30619  elicoelioo  33064  cndprobprob  34773  bnj543  35226  cusgr3cyclex  35527  ellimits  36299  eldmxrncnvepres  38973  eldmxrncnvepres2  38974  refsymrel2  39190  refsymrel3  39191  dfeqvrel2  39213  dfeqvrel3  39214  i0oii  49583