Theorem 3anan32 1095

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 1087	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32 642	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	1, 2	bitri 274	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  3ancomb  1097  anandi3r  1101  rabssrabd  4080  dff1o3  6838  bropfvvvvlem  8079  tz7.49c  8448  ispos2  18272  lbsacsbs  20914  obslbs  21504  islbs4  21606  leordtvallem1  22934  trfbas2  23567  isclmp  24844  lssbn  25100  sineq0  26269  dchrelbas3  26977  elno3  27394  nb3grpr2  28907  uspgr2wlkeq  29170  2spthd  29462  clwwlknonwwlknonb  29626  frgr2wwlkeu  29847  elicoelioo  32256  cndprobprob  33735  bnj543  34202  cusgr3cyclex  34425  ellimits  35186  refsymrel2  37740  refsymrel3  37741  dfeqvrel2  37763  dfeqvrel3  37764  i0oii  47639