![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon3ai | Structured version Visualization version GIF version |
Description: Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
necon3ai.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
necon3ai | ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3ai.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | nne 2972 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
3 | 1, 2 | sylibr 226 | . 2 ⊢ (𝜑 → ¬ 𝐴 ≠ 𝐵) |
4 | 3 | con2i 137 | 1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1601 ≠ wne 2968 |
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 199 df-ne 2969 |
This theorem is referenced by: necon1ai 2995 necon3i 3000 neneor 3070 nelsn 4433 disjsn2 4478 prnesn 4622 opelopabsb 5222 funsndifnop 6682 map0b 8181 mapdom3 8420 cflim2 9420 isfin4-3 9472 fpwwe2lem13 9799 tskuni 9940 recextlem2 11006 hashprg 13497 eqsqrt2d 14515 gcd1 15655 gcdzeq 15677 lcmfunsnlem2lem1 15757 lcmfunsnlem2lem2 15758 phimullem 15888 pcgcd1 15985 pc2dvds 15987 pockthlem 16013 ablfacrplem 18851 znrrg 20309 opnfbas 22054 supfil 22107 itg1addlem4 23903 itg1addlem5 23904 dvdsmulf1o 25372 ppiub 25381 dchrelbas4 25420 lgsne0 25512 2sqlem8 25603 tgldimor 25853 subfacp1lem6 31766 cvmsss2 31855 ax6e2ndeq 39701 supminfxr2 40586 fourierdlem56 41288 |
Copyright terms: Public domain | W3C validator |