![]() |
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 3001. (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 2999 | . 2 ⊢ 𝐵 ≠ 𝐴 |
3 | 2 | neii 2946 | 1 ⊢ ¬ 𝐵 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1542 ≠ wne 2944 |
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 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2729 df-ne 2945 |
This theorem is referenced by: 0nelopab 5529 0nelxp 5672 1sdom2dom 9198 recgt0ii 12068 xrltnr 13047 nltmnf 13057 xnn0xadd0 13173 fnpr2ob 17447 setcepi 17981 pmtrprfval 19276 pmtrprfvalrn 19277 cnfldfun 20824 zringndrg 20905 vieta1lem2 25687 2lgslem3 26768 2lgslem4 26770 sltval2 27020 nosgnn0 27022 nogt01o 27060 structiedg0val 28015 snstriedgval 28031 rusgrnumwwlkl1 28955 clwwlknon1sn 29086 frgrreggt1 29379 1nei 31695 ballotlemi1 33142 sgnnbi 33185 sgnpbi 33186 plymulx0 33199 fmlaomn0 34024 fmla0disjsuc 34032 fmlasucdisj 34033 bj-0nel1 35453 bj-0nelsngl 35471 bj-pr22val 35519 bj-pinftynminfty 35727 finxp0 35891 wepwsolem 41398 refsum2cnlem1 43316 spr0nelg 45742 oddprmALTV 45953 |
Copyright terms: Public domain | W3C validator |