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

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

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 1105

This theorem is referenced by:  3ancomb  1116  anandi3r  1120  rabssrabd  4037  dff1o3  6827  bropfvvvvlem  8082  tz7.49c  8429  ispos2  18366  lbsacsbs  21280  obslbs  21880  islbs4  21982  leordtvallem1  23367  trfbas2  24000  isclmp  25256  lssbn  25511  sineq0  26689  dchrelbas3  27402  elno3  27819  nb3grpr2  29733  uspgr2wlkeq  29995  2spthd  30290  clwwlknonwwlknonb  30457  frgr2wwlkeu  30678  elicoelioo  33123  cndprobprob  34828  bnj543  35281  cusgr3cyclex  35628  ellimits  36400  eldmxrncnvepres  39103  eldmxrncnvepres2  39104  refsymrel2  39320  refsymrel3  39321  dfeqvrel2  39343  dfeqvrel3  39344  i0oii  49718