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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3ancomb  1098  anandi3r  1102  rabssrabd  4016  dff1o3  6722  bropfvvvvlem  7931  tz7.49c  8277  ispos2  18033  lbsacsbs  20418  obslbs  20937  islbs4  21039  leordtvallem1  22361  trfbas2  22994  isclmp  24260  lssbn  24516  sineq0  25680  dchrelbas3  26386  nb3grpr2  27750  uspgr2wlkeq  28013  2spthd  28306  clwwlknonwwlknonb  28470  frgr2wwlkeu  28691  elicoelioo  31099  cndprobprob  32405  bnj543  32873  cusgr3cyclex  33098  elno3  33858  ellimits  34212  refsymrel2  36681  refsymrel3  36682  dfeqvrel2  36703  dfeqvrel3  36704  i0oii  46213