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 3066 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) | |
3 | 1, 2 | mpbi 231 | 1 ⊢ 𝐵 ≠ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 3013 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-ne 3014 |
This theorem is referenced by: nesymi 3070 nesymir 3071 0nep0 5249 opthhausdorff 5398 xp01disj 8109 xp01disjl 8110 1sdom 8709 djuexb 9326 djuin 9335 pnfnemnf 10684 mnfnepnf 10685 ltneii 10741 0ne1 11696 0ne2 11832 xnn0n0n1ge2b 12514 xmulpnf1 12655 fzprval 12956 hashneq0 13713 f1oun2prg 14267 geo2sum2 15218 fnpr2o 16818 fvpr0o 16820 fvpr1o 16821 rescabs 17091 dmdprdpr 19100 dprdpr 19101 mgpress 19179 cnfldfunALT 20486 xpstopnlem1 22345 2logb9irrALT 25303 sqrt2cxp2logb9e3 25304 1sgm2ppw 25703 2sqlem11 25932 axlowdimlem13 26667 usgrexmpldifpr 26967 usgrexmplef 26968 vdegp1ai 27245 vdegp1bi 27246 konigsbergiedgw 27954 konigsberglem2 27959 konigsberglem3 27960 ex-pss 28134 ex-hash 28159 signswch 31730 nosepnelem 33081 bj-disjsn01 34161 bj-1upln0 34218 finxpreclem3 34556 remul01 39115 mnuprdlem2 40486 ovnsubadd2lem 42804 nnlog2ge0lt1 44554 logbpw2m1 44555 fllog2 44556 blennnelnn 44564 nnpw2blen 44568 blen1 44572 blen2 44573 blen1b 44576 blennnt2 44577 nnolog2flm1 44578 blennngt2o2 44580 blennn0e2 44582 inlinecirc02plem 44701 |
Copyright terms: Public domain | W3C validator |