![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nesym | Structured version Visualization version GIF version |
Description: Characterization of inequality in terms of reversed equality (see bicom 222). (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
nesym | ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2742 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
2 | 1 | necon3abii 2985 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 206 = wceq 1537 ≠ wne 2938 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-cleq 2727 df-ne 2939 |
This theorem is referenced by: ord1eln01 8533 ord2eln012 8534 fiming 9536 wemapsolem 9588 nn01to3 12981 xrltlen 13185 sgnn 15130 isprm3 16717 lspsncv0 21166 uvcvv0 21828 fvmptnn04if 22871 chfacfisf 22876 chfacfisfcpmat 22877 trfbas 23868 fbunfip 23893 trfil2 23911 iundisj2 25598 nosupbnd2lem1 27775 noinfbnd2lem1 27790 elnns2 28359 pthdlem2lem 29800 fusgr2wsp2nb 30363 iundisj2f 32610 iundisj2fi 32805 cvmscld 35258 poimirlem25 37632 hlrelat5N 39384 redvmptabs 42369 cmpfiiin 42685 gneispace 44124 iblcncfioo 45934 fourierdlem82 46144 elprneb 46979 fzopredsuc 47273 iccpartiltu 47347 |
Copyright terms: Public domain | W3C validator |