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 3069. (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 3067 | . 2 ⊢ 𝐵 ≠ 𝐴 |
3 | 2 | neii 3015 | 1 ⊢ ¬ 𝐵 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1528 ≠ wne 3013 |
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 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-ne 3014 |
This theorem is referenced by: 0nelxp 5582 recgt0ii 11534 xrltnr 12502 nltmnf 12512 xnn0xadd0 12628 fnpr2ob 16819 setcepi 17336 pmtrprfval 18544 pmtrprfvalrn 18545 cnfldfunALT 20486 zringndrg 20565 vieta1lem2 24827 2lgslem3 25907 2lgslem4 25909 structiedg0val 26734 snstriedgval 26750 rusgrnumwwlkl1 27674 clwwlknon1sn 27806 frgrreggt1 28099 1nei 30398 ballotlemi1 31659 sgnnbi 31702 sgnpbi 31703 plymulx0 31716 fmlaomn0 32534 fmla0disjsuc 32542 fmlasucdisj 32543 sltval2 33060 nosgnn0 33062 bj-0nel1 34162 bj-0nelsngl 34180 bj-pr22val 34228 bj-pinftynminfty 34401 finxp0 34554 wepwsolem 39520 refsum2cnlem1 41171 spr0nelg 43515 oddprmALTV 43729 |
Copyright terms: Public domain | W3C validator |