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 3017. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
neii.1 | ⊢ 𝐴 ≠ 𝐵 |
Ref | Expression |
---|---|
neii | ⊢ ¬ 𝐴 = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neii.1 | . 2 ⊢ 𝐴 ≠ 𝐵 | |
2 | df-ne 3017 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | mpbi 232 | 1 ⊢ ¬ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1537 ≠ wne 3016 |
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 209 df-ne 3017 |
This theorem is referenced by: nesymi 3073 nemtbir 3112 snsssn 4772 2dom 8582 map2xp 8687 updjudhcoinrg 9362 pm54.43lem 9428 canthp1lem2 10075 ine0 11075 inelr 11628 xrltnr 12515 pnfnlt 12524 prprrab 13832 wrdlen2i 14304 3lcm2e6woprm 15959 6lcm4e12 15960 m1dvdsndvds 16135 fnpr2ob 16831 fvprif 16834 pmatcollpw3fi1lem1 21394 sinhalfpilem 25049 coseq1 25110 2lgslem3 25980 2lgslem4 25982 axlowdimlem13 26740 axlowdim1 26745 umgredgnlp 26932 wwlksnext 27671 norm1exi 29027 largei 30044 ind1a 31278 ballotlemii 31761 sgnnbi 31803 sgnpbi 31804 gonanegoal 32599 gonan0 32639 goaln0 32640 fmlasucdisj 32646 ex-sategoelelomsuc 32673 ex-sategoelel12 32674 dfrdg2 33040 sltval2 33163 nosgnn0 33165 sltintdifex 33168 sltres 33169 sltsolem1 33180 nolt02o 33199 dfrdg4 33412 bj-1nel0 34269 bj-pr21val 34328 finxpreclem2 34674 epnsymrel 35813 0dioph 39395 clsk1indlem1 40415 dirkercncflem2 42409 fourierdlem60 42471 fourierdlem61 42472 afv20defat 43451 fun2dmnopgexmpl 43503 line2ylem 44758 |
Copyright terms: Public domain | W3C validator |