|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > necon2ai | Structured version Visualization version GIF version | ||
| Description: Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) | 
| Ref | Expression | 
|---|---|
| necon2ai.1 | ⊢ (𝐴 = 𝐵 → ¬ 𝜑) | 
| Ref | Expression | 
|---|---|
| necon2ai | ⊢ (𝜑 → 𝐴 ≠ 𝐵) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | necon2ai.1 | . . 3 ⊢ (𝐴 = 𝐵 → ¬ 𝜑) | |
| 2 | 1 | con2i 139 | . 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵) | 
| 3 | 2 | neqned 2947 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ≠ wne 2940 | 
| 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 207 df-ne 2941 | 
| This theorem is referenced by: necon2i 2975 intex 5344 iin0 5362 opelopabsb 5535 0ellim 6447 xpord2indlem 8172 ord1eln01 8534 ord2eln012 8535 1ellim 8536 2ellim 8537 0sdom1dom 9274 inf3lem3 9670 cardmin2 10039 pm54.43 10041 pr2ne 10044 canthp1lem2 10693 renepnf 11309 renemnf 11310 lt0ne0d 11828 nnne0ALT 12304 nn0nepnf 12607 hashnemnf 14383 hashnn0n0nn 14430 geolim 15906 geolim2 15907 georeclim 15908 geoisumr 15914 geoisum1c 15916 ramtcl2 17049 lhop1 26053 logdmn0 26682 logcnlem3 26686 bday1s 27876 lrold 27935 mulsval 28135 nbgrssovtx 29378 rusgrnumwwlkl1 29988 strlem1 32269 subfacp1lem1 35184 gonan0 35397 goaln0 35398 rankeq1o 36172 poimirlem9 37636 poimirlem18 37645 poimirlem19 37646 poimirlem20 37647 poimirlem32 37659 pssn0 42266 ensucne0 43542 fouriersw 46246 afvvfveq 47160 fdomne0 48759 | 
| Copyright terms: Public domain | W3C validator |