NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  simplr Unicode 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  6229  lemuc1  6252  ncslesuc  6266  spacind  6285  nchoicelem8  6294  nchoicelem19  6305  nchoice  6306  fnfrec  6318
  Copyright terms: Public domain W3C validator