Theorem 3anan32 1097

Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Assertion

Ref	Expression
3anan32	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Proof of Theorem 3anan32

Step	Hyp	Ref	Expression
1		df-3an 1089	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32 647	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	1, 2	bitri 275	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3ancomb  1099  anandi3r  1103  rabssrabd  4023  dff1o3  6786  bropfvvvvlem  8041  tz7.49c  8385  ispos2  18281  lbsacsbs  21154  obslbs  21710  islbs4  21812  leordtvallem1  23175  trfbas2  23808  isclmp  25064  lssbn  25319  sineq0  26488  dchrelbas3  27201  elno3  27619  nb3grpr2  29452  uspgr2wlkeq  29714  2spthd  30009  clwwlknonwwlknonb  30176  frgr2wwlkeu  30397  elicoelioo  32851  cndprobprob  34582  bnj543  35035  cusgr3cyclex  35318  ellimits  36090  eldmxrncnvepres  38755  eldmxrncnvepres2  38756  refsymrel2  38972  refsymrel3  38973  dfeqvrel2  38995  dfeqvrel3  38996  i0oii  49395