![]() |
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 2988. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
neii.1 | ⊢ 𝐴 ≠ 𝐵 |
Ref | Expression |
---|---|
neii | ⊢ ¬ 𝐴 = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neii.1 | . 2 ⊢ 𝐴 ≠ 𝐵 | |
2 | df-ne 2988 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | mpbi 233 | 1 ⊢ ¬ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1538 ≠ wne 2987 |
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 210 df-ne 2988 |
This theorem is referenced by: nesymi 3044 nemtbir 3082 snsssn 4732 2dom 8565 map2xp 8671 updjudhcoinrg 9346 pm54.43lem 9413 canthp1lem2 10064 ine0 11064 inelr 11615 xrltnr 12502 pnfnlt 12511 prprrab 13827 wrdlen2i 14295 3lcm2e6woprm 15949 6lcm4e12 15950 m1dvdsndvds 16125 fnpr2ob 16823 fvprif 16826 pmatcollpw3fi1lem1 21391 sinhalfpilem 25056 coseq1 25117 2lgslem3 25988 2lgslem4 25990 axlowdimlem13 26748 axlowdim1 26753 umgredgnlp 26940 wwlksnext 27679 norm1exi 29033 largei 30050 ind1a 31388 ballotlemii 31871 sgnnbi 31913 sgnpbi 31914 gonanegoal 32712 gonan0 32752 goaln0 32753 fmlasucdisj 32759 ex-sategoelelomsuc 32786 ex-sategoelel12 32787 dfrdg2 33153 sltval2 33276 nosgnn0 33278 sltintdifex 33281 sltres 33282 sltsolem1 33293 nolt02o 33312 dfrdg4 33525 bj-1nel0 34390 bj-pr21val 34449 finxpreclem2 34807 epnsymrel 35958 sn-inelr 39590 0dioph 39719 clsk1indlem1 40748 dirkercncflem2 42746 fourierdlem60 42808 fourierdlem61 42809 afv20defat 43788 fun2dmnopgexmpl 43840 itcoval1 45077 line2ylem 45165 |
Copyright terms: Public domain | W3C validator |