![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nesymi | Structured version Visualization version GIF version |
Description: Inference associated with nesym 2997. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
Ref | Expression |
---|---|
nesymi.1 | ⊢ 𝐴 ≠ 𝐵 |
Ref | Expression |
---|---|
nesymi | ⊢ ¬ 𝐵 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nesymi.1 | . . 3 ⊢ 𝐴 ≠ 𝐵 | |
2 | 1 | necomi 2995 | . 2 ⊢ 𝐵 ≠ 𝐴 |
3 | 2 | neii 2942 | 1 ⊢ ¬ 𝐵 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1541 ≠ wne 2940 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2724 df-ne 2941 |
This theorem is referenced by: 0nelopab 5566 0nelxp 5709 1sdom2dom 9243 recgt0ii 12116 xrltnr 13095 nltmnf 13105 xnn0xadd0 13222 fnpr2ob 17500 setcepi 18034 pmtrprfval 19349 pmtrprfvalrn 19350 cnfldfun 20948 zringndrg 21029 vieta1lem2 25815 2lgslem3 26896 2lgslem4 26898 sltval2 27148 nosgnn0 27150 nogt01o 27188 structiedg0val 28271 snstriedgval 28287 rusgrnumwwlkl1 29211 clwwlknon1sn 29342 frgrreggt1 29635 1nei 31948 ballotlemi1 33489 sgnnbi 33532 sgnpbi 33533 plymulx0 33546 fmlaomn0 34369 fmla0disjsuc 34377 fmlasucdisj 34378 bj-0nel1 35822 bj-0nelsngl 35840 bj-pr22val 35888 bj-pinftynminfty 36096 finxp0 36260 wepwsolem 41769 refsum2cnlem1 43706 spr0nelg 46130 oddprmALTV 46341 |
Copyright terms: Public domain | W3C validator |