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

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

Proof of Theorem simp2
StepHypRef Expression
1 3simpa 952 . 2 ((φ ψ χ) → (φ ψ))
21simprd 449 1 ((φ ψ χ) → ψ)
 Colors of variables: wff setvar class 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:  simpl2  959  simpr2  962  simp2i  965  simp2d  968  simp12  986  simp22  989  simp32  992  syld3an3  1227  opkthg  4131  nnsucelrlem3  4426  ltfintri  4466  ncfindi  4475  sfintfin  4532  vfintle  4546  phi11lem1  4595  fvopab4t  5385  xpassen  6057  nenpw1pwlem2  6085  ceclnn1  6189  spacssnc  6284  spaccl  6286  nchoicelem17  6305
 Copyright terms: Public domain W3C validator