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

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

Proof of Theorem simprl
StepHypRef Expression
1 id 19 . 2 (ψψ)
21ad2antrl 708 1 ((φ (ψ χ)) → ψ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   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:  simp1rl  1020  simp2rl  1024  simp3rl  1028  rmob  3134  prepeano4  4451  preaddccan2  4455  tfin11  4493  tfinltfin  4501  evenodddisj  4516  sfindbl  4530  tfinnn  4534  vfinspsslem1  4550  vfinspclt  4552  xp0r  4842  weds  5938  ertr  5954  erth  5968  enadj  6060  enprmaplem3  6078  nntccl  6170  sbthlem3  6205  sbth  6206  tlecg  6230  nchoicelem6  6294  nchoicelem8  6296  nchoicelem19  6307  nchoice  6308
  Copyright terms: Public domain W3C validator