Theorem an32 564

Description: A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)

Assertion

Ref	Expression
an32	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Proof of Theorem an32

Step	Hyp	Ref	Expression
1		anass 401	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12 563	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3		ancom 266	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
4	1, 2, 3	3bitri 206	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an32s  570  3anan32  1016  indifdir  3477  inrab2  3494  reupick  3505  unidif0  4280  resco  5267  f11o  5648  respreima  5805  dff1o6  5949  dfoprab2  6100  xpassen  7081  enq0enq  7746  elioomnf  10301  modfsummod  12144  pcqcl  13004  ballotfilem2  13142  tx1cn  15134  isms2  15319  elcncf1di  15444