![]() |
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 2972. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
neii.1 | ⊢ 𝐴 ≠ 𝐵 |
Ref | Expression |
---|---|
neii | ⊢ ¬ 𝐴 = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neii.1 | . 2 ⊢ 𝐴 ≠ 𝐵 | |
2 | df-ne 2972 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | mpbi 222 | 1 ⊢ ¬ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1653 ≠ wne 2971 |
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 199 df-ne 2972 |
This theorem is referenced by: nesymi 3028 nemtbir 3066 snsssn 4558 2dom 8268 map2xp 8372 updjudhcoinrg 9045 pm54.43lem 9111 canthp1lem2 9763 ine0 10757 inelr 11302 xrltnr 12200 pnfnlt 12209 prprrab 13504 wrdlen2i 14027 3lcm2e6woprm 15663 6lcm4e12 15664 m1dvdsndvds 15836 xpsfrnel2 16540 pmatcollpw3fi1lem1 20919 sinhalfpilem 24557 coseq1 24616 2lgslem3 25481 2lgslem4 25483 axlowdimlem13 26191 axlowdim1 26196 umgredgnlp 26383 wwlksnext 27162 norm1exi 28632 largei 29651 ind1a 30597 ballotlemii 31082 sgnnbi 31124 sgnpbi 31125 dfrdg2 32213 sltval2 32322 nosgnn0 32324 sltintdifex 32327 sltres 32328 sltsolem1 32339 nolt02o 32358 dfrdg4 32571 bj-1nel0 33433 bj-pr21val 33493 finxpreclem2 33725 epnsymrel 34802 0dioph 38128 clsk1indlem1 39125 dirkercncflem2 41064 fourierdlem60 41126 fourierdlem61 41127 afv20defat 42086 fun2dmnopgexmpl 42139 |
Copyright terms: Public domain | W3C validator |