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

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

Proof of Theorem simplr
StepHypRef Expression
1 id 19 . 2 (ψψ)
21ad2antlr 707 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:  simp1lr  1019  simp2lr  1023  simp3lr  1027  ax11indalem  2197  ax11inda2ALT  2198  ifboth  3693  intab  3956  prepeano4  4451  leltfintr  4458  lenltfin  4469  tfinnn  4534  phi11lem1  4595  imainss  5042  ncssfin  6151  nntccl  6170  sbth  6206  leconnnc  6218  tlecg  6230  lemuc1  6253  ncslesuc  6267  spacind  6287  nchoicelem8  6296  nchoicelem19  6307  nchoice  6308  fnfrec  6320
  Copyright terms: Public domain W3C validator