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  4007  dff1o3  6836  bropfvvvvlem  8107  tz7.49c  8464  ispos2  18498  lbsacsbs  21443  obslbs  22045  islbs4  22147  leordtvallem1  23537  trfbas2  24171  isclmp  25427  lssbn  25682  sineq0  26861  dchrelbas3  27574  elno3  28021  nb3grpr2  29973  uspgr2wlkeq  30235  2spthd  30539  clwwlknonwwlknonb  30706  frgr2wwlkeu  30937  elicoelioo  33420  cndprobprob  35120  bnj543  35573  cusgr3cyclex  36019  ellimits  36796  eldmxrncnvepres  39503  eldmxrncnvepres2  39504  refsymrel2  39720  refsymrel3  39721  dfeqvrel2  39743  dfeqvrel3  39744  i0oii  50170