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  4082  dff1o3  6853  bropfvvvvlem  8117  tz7.49c  8487  ispos2  18362  lbsacsbs  21159  obslbs  21751  islbs4  21853  leordtvallem1  23219  trfbas2  23852  isclmp  25131  lssbn  25387  sineq0  26567  dchrelbas3  27283  elno3  27701  nb3grpr2  29401  uspgr2wlkeq  29665  2spthd  29962  clwwlknonwwlknonb  30126  frgr2wwlkeu  30347  elicoelioo  32781  cndprobprob  34441  bnj543  34908  cusgr3cyclex  35142  ellimits  35912  refsymrel2  38569  refsymrel3  38570  dfeqvrel2  38592  dfeqvrel3  38593  i0oii  48824