New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > simprbi | Unicode version |
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.) |
Ref | Expression |
---|---|
simprbi.1 |
Ref | Expression |
---|---|
simprbi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprbi.1 | . . 3 | |
2 | 1 | biimpi 186 | . 2 |
3 | 2 | simprd 449 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 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: sb1 1651 eumo 2244 2eu1 2284 reurmo 2826 pssne 3365 pssn2lp 3370 ssnpss 3372 eldifn 3389 rabsnt 3797 eldifsni 3840 unimax 3925 ssintub 3944 dfnnc2 4395 nnsucelr 4428 ssfin 4470 vfinspsslem1 4550 opeliunxp 4820 opeldm 4910 dmsnopss 5067 fndm 5182 frn 5228 f1ss 5262 forn 5272 f1f1orn 5297 f1orescnv 5301 f1imacnv 5302 fun11iun 5305 tz6.12-2 5346 foelrn 5425 f1fveq 5473 isorel 5489 isoini2 5498 2ndfo 5506 fovcl 5588 weds 5938 ertr 5954 ertrd 5955 en0 6042 enpw1 6062 ncdisjun 6136 nchoicelem8 6296 nchoicelem15 6303 frecxp 6314 dmfrec 6316 fnfreclem2 6318 |
Copyright terms: Public domain | W3C validator |