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 2782. (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
neii.1 | ⊢ 𝐴 ≠ 𝐵 |
Ref | Expression |
---|---|
neii | ⊢ ¬ 𝐴 = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neii.1 | . 2 ⊢ 𝐴 ≠ 𝐵 | |
2 | df-ne 2782 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | mpbi 219 | 1 ⊢ ¬ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1475 ≠ wne 2780 |
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 196 df-ne 2782 |
This theorem is referenced by: nesymi 2839 nemtbir 2877 snsssn 4312 2dom 7915 map2xp 8015 pm54.43lem 8708 canthp1lem2 9354 ine0 10344 inelr 10887 xrltnr 11829 pnfnlt 11838 prprrab 13112 wrdlen2i 13534 3lcm2e6woprm 15166 6lcm4e12 15167 m1dvdsndvds 15341 xpsfrnel2 16048 pmatcollpw3fi1lem1 20410 sinhalfpilem 24019 coseq1 24078 2lgslem3 24929 2lgslem4 24931 axlowdimlem13 25634 axlowdim1 25639 umgredgnlp 25818 usgraedgprv 25905 wlkntrllem3 26091 4cycl4dv 26195 wwlknext 26252 norm1exi 27491 largei 28510 ind1a 29410 ballotlemii 29892 sgnnbi 29934 sgnpbi 29935 dfrdg2 30945 sltval2 31053 nosgnn0 31055 sltintdifex 31060 sltres 31061 sltsolem1 31067 dfrdg4 31228 bj-1nel0 32134 bj-pr21val 32194 finxpreclem2 32403 0dioph 36360 clsk1indlem1 37363 dirkercncflem2 38997 fourierdlem60 39059 fourierdlem61 39060 fun2dmnopgexmpl 40329 uvtxa01vtx 40624 wwlksnext 41099 |
Copyright terms: Public domain | W3C validator |