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 3072. (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 3070 | . 2 ⊢ 𝐵 ≠ 𝐴 |
3 | 2 | neii 3018 | 1 ⊢ ¬ 𝐵 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1528 ≠ wne 3016 |
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 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-ne 3017 |
This theorem is referenced by: 0nelxp 5583 recgt0ii 11535 xrltnr 12504 nltmnf 12514 xnn0xadd0 12630 fnpr2ob 16821 setcepi 17338 pmtrprfval 18546 pmtrprfvalrn 18547 cnfldfunALT 20488 zringndrg 20567 vieta1lem2 24829 2lgslem3 25908 2lgslem4 25910 structiedg0val 26735 snstriedgval 26751 rusgrnumwwlkl1 27675 clwwlknon1sn 27807 frgrreggt1 28100 1nei 30399 ballotlemi1 31660 sgnnbi 31703 sgnpbi 31704 plymulx0 31717 fmlaomn0 32535 fmla0disjsuc 32543 fmlasucdisj 32544 sltval2 33061 nosgnn0 33063 bj-0nel1 34163 bj-0nelsngl 34181 bj-pr22val 34229 bj-pinftynminfty 34402 finxp0 34555 wepwsolem 39522 refsum2cnlem1 41174 spr0nelg 43485 oddprmALTV 43699 |
Copyright terms: Public domain | W3C validator |