![]() |
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 2998. (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 2996 | . 2 ⊢ 𝐵 ≠ 𝐴 |
3 | 2 | neii 2943 | 1 ⊢ ¬ 𝐵 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1542 ≠ wne 2941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 df-ne 2942 |
This theorem is referenced by: 0nelopab 5568 0nelxp 5711 1sdom2dom 9247 recgt0ii 12120 xrltnr 13099 nltmnf 13109 xnn0xadd0 13226 fnpr2ob 17504 setcepi 18038 pmtrprfval 19355 pmtrprfvalrn 19356 cnfldfun 20956 zringndrg 21038 vieta1lem2 25824 2lgslem3 26907 2lgslem4 26909 sltval2 27159 nosgnn0 27161 nogt01o 27199 structiedg0val 28313 snstriedgval 28329 rusgrnumwwlkl1 29253 clwwlknon1sn 29384 frgrreggt1 29677 1nei 31992 ballotlemi1 33532 sgnnbi 33575 sgnpbi 33576 plymulx0 33589 fmlaomn0 34412 fmla0disjsuc 34420 fmlasucdisj 34421 gg-cnfldfun 35228 bj-0nel1 35882 bj-0nelsngl 35900 bj-pr22val 35948 bj-pinftynminfty 36156 finxp0 36320 wepwsolem 41832 refsum2cnlem1 43769 spr0nelg 46192 oddprmALTV 46403 |
Copyright terms: Public domain | W3C validator |