Theorem an4 797

Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)

Assertion

Ref	Expression
an4	⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) ↔ ((φ ∧ χ) ∧ (ψ ∧ θ)))

Proof of Theorem an4

Step	Hyp	Ref	Expression
1		an12 772	. . 3 ⊢ ((ψ ∧ (χ ∧ θ)) ↔ (χ ∧ (ψ ∧ θ)))
2	1	anbi2i 675	. 2 ⊢ ((φ ∧ (ψ ∧ (χ ∧ θ))) ↔ (φ ∧ (χ ∧ (ψ ∧ θ))))
3		anass 630	. 2 ⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) ↔ (φ ∧ (ψ ∧ (χ ∧ θ))))
4		anass 630	. 2 ⊢ (((φ ∧ χ) ∧ (ψ ∧ θ)) ↔ (φ ∧ (χ ∧ (ψ ∧ θ))))
5	2, 3, 4	3bitr4i 268	1 ⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) ↔ ((φ ∧ χ) ∧ (ψ ∧ θ)))

Syntax hints:   ↔ wb 176   ∧ wa 358

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 177  df-an 360

This theorem is referenced by:  an42  798  an4s  799  anandi  801  anandir  802  rnlem  931  an6  1261  2eu1  2284  2eu4  2287  reean  2777  reu2  3024  rmo4  3029  rmo3  3133  inxpk  4277  dfpw12  4301  ltfintr  4459  opelxp  4811  inxp  4863  xp11  5056  fununi  5160  2elresin  5194  fun  5236  resoprab2  5582  brtxp  5783  qrpprod  5836  fundmen  6043