Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simplbi2com | Structured version Visualization version Unicode version |
Description: A deduction eliminating a conjunct, similar to simplbi2 655. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.) |
Ref | Expression |
---|---|
simplbi2com.1 |
Ref | Expression |
---|---|
simplbi2com |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplbi2com.1 | . . 3 | |
2 | 1 | simplbi2 655 | . 2 |
3 | 2 | com12 32 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 |
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 197 df-an 386 |
This theorem is referenced by: elres 5435 xpidtr 5518 elovmpt2rab 6880 elovmpt2rab1 6881 inficl 8331 cfslb2n 9090 repswcshw 13558 cshw1 13568 bezoutlem1 15256 bezoutlem3 15258 modprmn0modprm0 15512 cnprest 21093 haust1 21156 lly1stc 21299 3cyclfrgrrn1 27149 dfon2lem9 31696 phpreu 33393 poimirlem26 33435 sb5ALT 38731 onfrALTlem2 38761 onfrALTlem2VD 39125 sb5ALTVD 39149 funcoressn 41207 ndmaovdistr 41287 2elfz3nn0 41326 reuccatpfxs1 41434 |
Copyright terms: Public domain | W3C validator |