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-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: 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 |