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 2838. (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 2836 | . 2 ⊢ 𝐵 ≠ 𝐴 |
3 | 2 | neii 2784 | 1 ⊢ ¬ 𝐵 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1475 ≠ wne 2780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-cleq 2603 df-ne 2782 |
This theorem is referenced by: 0nelxp 5067 recgt0ii 10808 xrltnr 11829 nltmnf 11839 xnn0xadd0 11949 setcepi 16561 pmtrprfval 17730 pmtrprfvalrn 17731 zringndrg 19657 vieta1lem2 23870 2lgslem3 24929 2lgslem4 24931 structiedg0val 25699 snstriedgval 25713 usgraedgprv 25905 2trllemA 26080 2pthon 26132 2pthon3v 26134 4cycl4dv 26195 rusgranumwlkl1 26474 frgrareggt1 26643 ballotlemi1 29891 sgnnbi 29934 sgnpbi 29935 plymulx0 29950 sltval2 31053 nosgnn0 31055 bj-0nel1 32133 bj-0nelsngl 32152 bj-pr22val 32200 bj-pinftynminfty 32291 finxp0 32404 wepwsolem 36630 refsum2cnlem1 38219 oddprmALTV 40136 rusgrnumwwlkl1 41172 av-frgrareggt1 41547 |
Copyright terms: Public domain | W3C validator |