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  4031  dff1o3  6831  bropfvvvvlem  8102  tz7.49c  8456  ispos2  18489  lbsacsbs  21434  obslbs  22036  islbs4  22138  leordtvallem1  23528  trfbas2  24162  isclmp  25418  lssbn  25673  sineq0  26852  dchrelbas3  27565  elno3  28012  nb3grpr2  29964  uspgr2wlkeq  30226  2spthd  30530  clwwlknonwwlknonb  30697  frgr2wwlkeu  30928  elicoelioo  33370  cndprobprob  35070  bnj543  35523  cusgr3cyclex  35911  ellimits  36672  eldmxrncnvepres  39366  eldmxrncnvepres2  39367  refsymrel2  39583  refsymrel3  39584  dfeqvrel2  39606  dfeqvrel3  39607  i0oii  50027