![]() |
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 2801 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
2 | 1 | necon3abii 3029 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 = wceq 1522 ≠ wne 2983 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-9 2090 ax-ext 2768 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1763 df-cleq 2787 df-ne 2984 |
This theorem is referenced by: 0nelopab 5343 fiming 8811 wemapsolem 8863 nn01to3 12190 xrltlen 12389 sgnn 14287 pwm1geoserOLD 15058 isprm3 15856 lspsncv0 19608 uvcvv0 20616 fvmptnn04if 21141 chfacfisf 21146 chfacfisfcpmat 21147 trfbas 22136 fbunfip 22161 trfil2 22179 iundisj2 23833 pthdlem2lem 27230 fusgr2wsp2nb 27797 iundisj2f 30022 iundisj2fi 30198 cvmscld 32122 nosupbnd2lem1 32818 poimirlem25 34461 hlrelat5N 36081 cmpfiiin 38792 gneispace 39982 iblcncfioo 41818 fourierdlem82 42029 elprneb 42794 fzopredsuc 43053 iccpartiltu 43078 |
Copyright terms: Public domain | W3C validator |