![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neii | Structured version Visualization version GIF version |
Description: Inference associated with df-ne 2930. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
neii.1 | ⊢ 𝐴 ≠ 𝐵 |
Ref | Expression |
---|---|
neii | ⊢ ¬ 𝐴 = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neii.1 | . 2 ⊢ 𝐴 ≠ 𝐵 | |
2 | df-ne 2930 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | mpbi 229 | 1 ⊢ ¬ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1533 ≠ wne 2929 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-ne 2930 |
This theorem is referenced by: nesymi 2987 nemtbir 3027 snsssn 4844 nlim1 8510 nlim2 8511 2dom 9055 map2xp 9172 snnen2o 9262 ssttrcl 9740 ttrclselem2 9751 updjudhcoinrg 9958 pm54.43lem 10025 canthp1lem2 10678 ine0 11681 inelr 12235 xrltnr 13134 pnfnlt 13143 prprrab 14470 wrdlen2i 14929 3lcm2e6woprm 16589 6lcm4e12 16590 m1dvdsndvds 16770 fnpr2ob 17543 fvprif 17546 pmatcollpw3fi1lem1 22732 sinhalfpilem 26443 coseq1 26504 2lgslem3 27382 2lgslem4 27384 sltval2 27635 nosgnn0 27637 sltintdifex 27640 sltres 27641 sltsolem1 27654 nolt02o 27674 nogt01o 27675 axlowdimlem13 28837 axlowdim1 28842 umgredgnlp 29032 wwlksnext 29776 norm1exi 31132 largei 32149 ind1a 33769 ballotlemii 34254 sgnnbi 34296 sgnpbi 34297 gonanegoal 35093 gonan0 35133 goaln0 35134 fmlasucdisj 35140 ex-sategoelelomsuc 35167 ex-sategoelel12 35168 dfrdg2 35522 dfrdg4 35678 bj-1nel0 36564 bj-pr21val 36623 finxpreclem2 37000 epnsymrel 38164 sn-inelr 42155 0dioph 42340 oaomoencom 42888 clsk1indlem1 43617 dirkercncflem2 45630 fourierdlem60 45692 fourierdlem61 45693 afv20defat 46750 fun2dmnopgexmpl 46802 itcoval1 47922 line2ylem 48010 |
Copyright terms: Public domain | W3C validator |