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 3069 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) | |
3 | 1, 2 | mpbi 231 | 1 ⊢ 𝐵 ≠ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 3016 |
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 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-ne 3017 |
This theorem is referenced by: nesymi 3073 nesymir 3074 0nep0 5250 opthhausdorff 5399 xp01disj 8111 xp01disjl 8112 1sdom 8710 djuexb 9327 djuin 9336 pnfnemnf 10685 mnfnepnf 10686 ltneii 10742 0ne1 11697 0ne2 11833 xnn0n0n1ge2b 12516 xmulpnf1 12657 fzprval 12958 hashneq0 13715 f1oun2prg 14269 geo2sum2 15220 fnpr2o 16820 fvpr0o 16822 fvpr1o 16823 rescabs 17093 dmdprdpr 19102 dprdpr 19103 mgpress 19181 cnfldfunALT 20488 xpstopnlem1 22347 2logb9irrALT 25303 sqrt2cxp2logb9e3 25304 1sgm2ppw 25704 2sqlem11 25933 axlowdimlem13 26668 usgrexmpldifpr 26968 usgrexmplef 26969 vdegp1ai 27246 vdegp1bi 27247 konigsbergiedgw 27955 konigsberglem2 27960 konigsberglem3 27961 ex-pss 28135 ex-hash 28160 signswch 31731 nosepnelem 33082 bj-disjsn01 34162 bj-1upln0 34219 finxpreclem3 34557 remul01 39117 mnuprdlem2 40489 ovnsubadd2lem 42808 nnlog2ge0lt1 44524 logbpw2m1 44525 fllog2 44526 blennnelnn 44534 nnpw2blen 44538 blen1 44542 blen2 44543 blen1b 44546 blennnt2 44547 nnolog2flm1 44548 blennngt2o2 44550 blennn0e2 44552 inlinecirc02plem 44671 |
Copyright terms: Public domain | W3C validator |