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 3067 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) | |
3 | 1, 2 | mpbi 232 | 1 ⊢ 𝐵 ≠ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 3014 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-9 2118 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1775 df-cleq 2812 df-ne 3015 |
This theorem is referenced by: nesymi 3071 nesymir 3072 0nep0 5249 opthhausdorff 5398 xp01disj 8112 xp01disjl 8113 1sdom 8713 djuexb 9330 djuin 9339 pnfnemnf 10688 mnfnepnf 10689 ltneii 10745 0ne1 11700 0ne2 11836 xnn0n0n1ge2b 12518 xmulpnf1 12659 fzprval 12960 hashneq0 13717 f1oun2prg 14271 geo2sum2 15222 fnpr2o 16822 fvpr0o 16824 fvpr1o 16825 rescabs 17095 symgvalstruct 18517 dmdprdpr 19163 dprdpr 19164 mgpress 19242 cnfldfunALT 20550 xpstopnlem1 22409 2logb9irrALT 25368 sqrt2cxp2logb9e3 25369 1sgm2ppw 25768 2sqlem11 25997 axlowdimlem13 26732 usgrexmpldifpr 27032 usgrexmplef 27033 vdegp1ai 27310 vdegp1bi 27311 konigsbergiedgw 28019 konigsberglem2 28024 konigsberglem3 28025 ex-pss 28199 ex-hash 28224 signswch 31824 nosepnelem 33177 bj-disjsn01 34257 bj-1upln0 34314 finxpreclem3 34666 remul01 39228 mnuprdlem2 40600 ovnsubadd2lem 42918 nnlog2ge0lt1 44617 logbpw2m1 44618 fllog2 44619 blennnelnn 44627 nnpw2blen 44631 blen1 44635 blen2 44636 blen1b 44639 blennnt2 44640 nnolog2flm1 44641 blennngt2o2 44643 blennn0e2 44645 inlinecirc02plem 44764 |
Copyright terms: Public domain | W3C validator |