Theorem 3anan32 1113

Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof 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  4011  dff1o3  6861  bropfvvvvlem  8137  tz7.49c  8494  ispos2  18539  lbsacsbs  21485  obslbs  22091  islbs4  22193  leordtvallem1  23583  trfbas2  24217  isclmp  25473  lssbn  25728  sineq0  26909  dchrelbas3  27622  elno3  28069  nb3grpr2  30021  uspgr2wlkeq  30283  2spthd  30587  clwwlknonwwlknonb  30754  frgr2wwlkeu  30985  elicoelioo  33466  cndprobprob  35181  bnj543  35634  cusgr3cyclex  36109  ellimits  36887  eldmxrncnvepres  39632  eldmxrncnvepres2  39633  refsymrel2  39849  refsymrel3  39850  dfeqvrel2  39872  dfeqvrel3  39873  i0oii  50365