New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > simplbi | Unicode version |
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.) |
Ref | Expression |
---|---|
simplbi.1 |
Ref | Expression |
---|---|
simplbi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplbi.1 | . . 3 | |
2 | 1 | biimpi 186 | . 2 |
3 | 2 | simpld 445 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 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: 3simpa 952 reurex 2825 eqimss 3323 pssss 3364 eldifi 3388 inss1 3475 ssunsn2 3865 fnfun 5181 ffn 5223 f1f 5258 f1of1 5286 f1ofo 5293 nfvres 5352 ressnop0 5436 isof1o 5488 1stfo 5505 oprabid 5550 brtxp 5783 otelins2 5791 otelins3 5792 oqelins4 5794 weds 5938 ersym 5952 nchoicelem4 6290 nchoicelem8 6294 nchoicelem9 6295 nchoicelem19 6305 fnfreclem3 6317 |
Copyright terms: Public domain | W3C validator |