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 223). (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
nesym | ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2828 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
2 | 1 | necon3abii 3062 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 = 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: 0nelopab 5444 fiming 8951 wemapsolem 9003 nn01to3 12330 xrltlen 12529 sgnn 14443 pwm1geoserOLD 15215 isprm3 16017 lspsncv0 19849 uvcvv0 20864 fvmptnn04if 21387 chfacfisf 21392 chfacfisfcpmat 21393 trfbas 22382 fbunfip 22407 trfil2 22425 iundisj2 24079 pthdlem2lem 27476 fusgr2wsp2nb 28041 iundisj2f 30269 iundisj2fi 30447 cvmscld 32418 nosupbnd2lem1 33113 poimirlem25 34799 hlrelat5N 36419 cmpfiiin 39174 gneispace 40364 iblcncfioo 42143 fourierdlem82 42354 elprneb 43145 fzopredsuc 43404 iccpartiltu 43429 |
Copyright terms: Public domain | W3C validator |