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  4042  dff1o3  6788  bropfvvvvlem  8047  tz7.49c  8391  ispos2  18256  lbsacsbs  21098  obslbs  21672  islbs4  21774  leordtvallem1  23130  trfbas2  23763  isclmp  25030  lssbn  25285  sineq0  26466  dchrelbas3  27182  elno3  27600  nb3grpr2  29363  uspgr2wlkeq  29626  2spthd  29921  clwwlknonwwlknonb  30085  frgr2wwlkeu  30306  elicoelioo  32751  cndprobprob  34422  bnj543  34876  cusgr3cyclex  35116  ellimits  35891  eldmxrncnvepres  38389  eldmxrncnvepres2  38390  refsymrel2  38551  refsymrel3  38552  dfeqvrel2  38574  dfeqvrel3  38575  i0oii  48901