![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necomi | Structured version Visualization version GIF 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 3052 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) | |
3 | 1, 2 | mpbi 222 | 1 ⊢ 𝐵 ≠ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 2999 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1881 df-cleq 2818 df-ne 3000 |
This theorem is referenced by: nesymi 3056 nesymir 3057 0nep0 5058 opthhausdorff 5203 xp01disj 7843 1sdom 8432 djuin 9057 pnfnemnf 10412 mnfnepnf 10413 ltneii 10469 0ne1 11422 0ne2 11565 xnn0n0n1ge2b 12251 xmulpnf1 12392 fzprval 12695 hashneq0 13445 f1oun2prg 14038 geo2sum2 14979 fprodn0f 15094 xpscfn 16572 xpsc0 16573 xpsc1 16574 rescabs 16845 dmdprdpr 18802 dprdpr 18803 mgpress 18854 cnfldfunALT 20119 xpstopnlem1 21983 2logb9irrALT 24938 sqrt2cxp2logb9e3 24939 1sgm2ppw 25338 2sqlem11 25567 axlowdimlem13 26253 usgrexmpldifpr 26555 usgrexmplef 26556 vdegp1ai 26834 vdegp1bi 26835 konigsbergiedgw 27627 konigsberglem2 27632 konigsberglem3 27633 ex-pss 27843 ex-hash 27868 signswch 31185 nosepnelem 32369 bj-disjsn01 33460 bj-1upln0 33519 finxpreclem3 33775 ovnsubadd2lem 41653 nnlog2ge0lt1 43207 logbpw2m1 43208 fllog2 43209 blennnelnn 43217 nnpw2blen 43221 blen1 43225 blen2 43226 blen1b 43229 blennnt2 43230 nnolog2flm1 43231 blennngt2o2 43233 blennn0e2 43235 |
Copyright terms: Public domain | W3C validator |