Theorem simp3 957

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp3	⊢ ((φ ∧ ψ ∧ χ) → χ)

Proof of Theorem simp3

Step	Hyp	Ref	Expression
1		3simpc 954	. 2 ⊢ ((φ ∧ ψ ∧ χ) → (ψ ∧ χ))
2	1	simprd 449	1 ⊢ ((φ ∧ ψ ∧ χ) → χ)

Syntax hints:   → wi 4   ∧ w3a 934

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  df-3an 936

This theorem is referenced by:  simpl3  960  simpr3  963  simp3i  966  simp3d  969  simp13  987  simp23  990  simp33  993  3anibar  1123  mob2  3016  opkthg  4131  ncfindi  4475  tfindi  4496  nnadjoinpw  4521  sfintfin  4532  tfinnn  4534  vfintle  4546  peano4  4557  fvopab4t  5385  f1oiso2  5500  ov2ag  5598  xpassen  6057  nenpw1pwlem2  6085  ceclnn1  6189  nclenc  6222  lenc  6223  taddc  6229  addcdir  6251  spaccl  6286