New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  simp3 GIF version

Theorem simp3 957
 Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
simp3 ((φ ψ χ) → χ)

Proof of Theorem simp3
StepHypRef Expression
1 3simpc 954 . 2 ((φ ψ χ) → (ψ χ))
21simprd 449 1 ((φ ψ χ) → χ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 934 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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
 Copyright terms: Public domain W3C validator