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  4032  dff1o3  6775  bropfvvvvlem  8027  tz7.49c  8371  ispos2  18227  lbsacsbs  21099  obslbs  21673  islbs4  21775  leordtvallem1  23131  trfbas2  23764  isclmp  25030  lssbn  25285  sineq0  26466  dchrelbas3  27182  elno3  27600  nb3grpr2  29368  uspgr2wlkeq  29631  2spthd  29926  clwwlknonwwlknonb  30093  frgr2wwlkeu  30314  elicoelioo  32768  cndprobprob  34458  bnj543  34912  cusgr3cyclex  35187  ellimits  35959  eldmxrncnvepres  38464  eldmxrncnvepres2  38465  refsymrel2  38669  refsymrel3  38670  dfeqvrel2  38692  dfeqvrel3  38693  i0oii  49025