Theorem 3anan32 1108

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  3ancomb  1111  anandi3r  1115  rabssrabd  4036  dff1o3  6813  bropfvvvvlem  8070  tz7.49c  8417  ispos2  18347  lbsacsbs  21226  obslbs  21782  islbs4  21884  leordtvallem1  23270  trfbas2  23903  isclmp  25159  lssbn  25414  sineq0  26589  dchrelbas3  27302  elno3  27719  nb3grpr2  29584  uspgr2wlkeq  29846  2spthd  30141  clwwlknonwwlknonb  30308  frgr2wwlkeu  30529  elicoelioo  32980  cndprobprob  34735  bnj543  35188  cusgr3cyclex  35486  ellimits  36258  eldmxrncnvepres  38933  eldmxrncnvepres2  38934  refsymrel2  39150  refsymrel3  39151  dfeqvrel2  39173  dfeqvrel3  39174  i0oii  49541