New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > simplr | Unicode version |
Description: Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.) |
Ref | Expression |
---|---|
simplr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 | |
2 | 1 | ad2antlr 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 |