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  6825  bropfvvvvlem  8089  tz7.49c  8436  ispos2  18404  lbsacsbs  21344  obslbs  21944  islbs4  22046  leordtvallem1  23436  trfbas2  24070  isclmp  25326  lssbn  25581  sineq0  26762  dchrelbas3  27475  elno3  27892  nb3grpr2  29844  uspgr2wlkeq  30106  2spthd  30410  clwwlknonwwlknonb  30577  frgr2wwlkeu  30808  elicoelioo  33250  cndprobprob  34950  bnj543  35403  cusgr3cyclex  35726  ellimits  36488  eldmxrncnvepres  39183  eldmxrncnvepres2  39184  refsymrel2  39400  refsymrel3  39401  dfeqvrel2  39423  dfeqvrel3  39424  i0oii  49847