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

Theorem simprr 733
Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
Assertion
Ref Expression
simprr ((φ (ψ χ)) → χ)

Proof of Theorem simprr
StepHypRef Expression
1 id 19 . 2 (χχ)
21ad2antll 709 1 ((φ (ψ χ)) → χ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358
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
This theorem is referenced by:  simp1rr  1021  simp2rr  1025  simp3rr  1029  prepeano4  4451  preaddccan2  4455  tfinltfin  4501  tfinnn  4534  vfinspsslem1  4550  weds  5938  ertr  5954  erth  5968  enadj  6060  enprmaplem3  6078  nntccl  6170  sbthlem1  6203  sbthlem3  6205  sbth  6206  tlecg  6230  nchoicelem6  6294  nchoicelem8  6296  nchoicelem19  6307  nchoice  6308
  Copyright terms: Public domain W3C validator