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 141 | . 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
3 | 2 | neqned 3023 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = 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: necon2i 3050 intex 5232 iin0 5253 opelopabsb 5409 0ellim 6247 inf3lem3 9082 cardmin2 9416 pm54.43 9418 canthp1lem2 10064 renepnf 10678 renemnf 10679 lt0ne0d 11194 nnne0ALT 11664 nn0nepnf 11964 hashnemnf 13694 hashnn0n0nn 13742 geolim 15216 geolim2 15217 georeclim 15218 geoisumr 15224 geoisum1c 15226 ramtcl2 16337 lhop1 24540 logdmn0 25150 logcnlem3 25154 nbgrssovtx 27071 rusgrnumwwlkl1 27675 strlem1 29955 subfacp1lem1 32324 gonan0 32537 goaln0 32538 rankeq1o 33530 poimirlem9 34783 poimirlem18 34792 poimirlem19 34793 poimirlem20 34794 poimirlem32 34806 pssn0 38993 ensucne0 39775 fouriersw 42397 afvvfveq 43228 |
Copyright terms: Public domain | W3C validator |