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 231 | 1 ⊢ ¬ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1528 ≠ 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 208 df-ne 3017 |
This theorem is referenced by: nesymi 3073 nemtbir 3112 snsssn 4766 2dom 8571 map2xp 8676 updjudhcoinrg 9351 pm54.43lem 9417 canthp1lem2 10064 ine0 11064 inelr 11617 xrltnr 12504 pnfnlt 12513 prprrab 13821 wrdlen2i 14294 3lcm2e6woprm 15949 6lcm4e12 15950 m1dvdsndvds 16125 fnpr2ob 16821 fvprif 16824 pmatcollpw3fi1lem1 21324 sinhalfpilem 24978 coseq1 25039 2lgslem3 25908 2lgslem4 25910 axlowdimlem13 26668 axlowdim1 26673 umgredgnlp 26860 wwlksnext 27599 norm1exi 28955 largei 29972 ind1a 31178 ballotlemii 31661 sgnnbi 31703 sgnpbi 31704 gonanegoal 32497 gonan0 32537 goaln0 32538 fmlasucdisj 32544 ex-sategoelelomsuc 32571 ex-sategoelel12 32572 dfrdg2 32938 sltval2 33061 nosgnn0 33063 sltintdifex 33066 sltres 33067 sltsolem1 33078 nolt02o 33097 dfrdg4 33310 bj-1nel0 34164 bj-pr21val 34223 finxpreclem2 34554 epnsymrel 35680 0dioph 39255 clsk1indlem1 40275 dirkercncflem2 42270 fourierdlem60 42332 fourierdlem61 42333 afv20defat 43312 fun2dmnopgexmpl 43364 line2ylem 44636 |
Copyright terms: Public domain | W3C validator |