![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necomi | Structured version Visualization version Unicode version |
Description: Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.) |
Ref | Expression |
---|---|
necomi.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
necomi |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necomi.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | necom 2688 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 213 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-cleq 2454 df-ne 2634 |
This theorem is referenced by: nesymi 2692 nesymir 2693 0nep0 4587 xp01disj 7223 1sdom 7800 ltneii 9772 0ne1 10704 0ne2 10849 pnfnemnf 11445 mnfnepnf 11446 xmulpnf1 11588 fzprval 11884 hashneq0 12576 f1oun2prg 13047 geo2sum2 13978 fprodn0f 14093 xpscfn 15513 xpsc0 15514 xpsc1 15515 rescabs 15786 dmdprdpr 17730 dprdpr 17731 mgpress 17782 xpstopnlem1 20872 1sgm2ppw 24176 2sqlem11 24351 axlowdimlem13 25032 usgraexmpldifpr 25175 usgraexmplef 25176 constr3lem4 25423 ex-pss 25926 signswch 29498 bj-disjsn01 31587 bj-1upln0 31647 finxpreclem3 31829 funvtxval 39165 nnlog2ge0lt1 40649 logbpw2m1 40650 fllog2 40651 blennnelnn 40659 nnpw2blen 40663 blen1 40667 blen2 40668 blen1b 40671 blennnt2 40672 nnolog2flm1 40673 blennngt2o2 40675 blennn0e2 40677 |
Copyright terms: Public domain | W3C validator |