Theorem 3anan32 1096

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 1088	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32 646	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	1, 2	bitri 275	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

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

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 1088

This theorem is referenced by:  3ancomb  1098  anandi3r  1102  rabssrabd  4030  dff1o3  6769  bropfvvvvlem  8021  tz7.49c  8365  ispos2  18221  lbsacsbs  21093  obslbs  21667  islbs4  21769  leordtvallem1  23125  trfbas2  23758  isclmp  25024  lssbn  25279  sineq0  26460  dchrelbas3  27176  elno3  27594  nb3grpr2  29361  uspgr2wlkeq  29624  2spthd  29919  clwwlknonwwlknonb  30086  frgr2wwlkeu  30307  elicoelioo  32761  cndprobprob  34451  bnj543  34905  cusgr3cyclex  35180  ellimits  35952  eldmxrncnvepres  38468  eldmxrncnvepres2  38469  refsymrel2  38673  refsymrel3  38674  dfeqvrel2  38696  dfeqvrel3  38697  i0oii  49030