![]() |
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.) (Proof shortened by Wolf Lammen, 28-Oct-2024.) |
Ref | Expression |
---|---|
necon3ai.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
necon3ai | ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neneq 2938 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) | |
2 | necon3ai.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
3 | 1, 2 | nsyl 140 | 1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1533 ≠ wne 2932 |
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 206 df-ne 2933 |
This theorem is referenced by: necon1ai 2960 necon3i 2965 neneor 3034 nelsn 4660 disjsn2 4708 prnesn 4852 opelopabsb 5520 funsndifnop 7141 ord1eln01 8491 map0b 8873 mapdom3 9145 cflim2 10254 isfin4p1 10306 fpwwe2lem12 10633 tskuni 10774 recextlem2 11842 hashprg 14352 eqsqrt2d 15312 gcd1 16466 gcdzeq 16491 lcmfunsnlem2lem1 16572 lcmfunsnlem2lem2 16573 phimullem 16711 pcgcd1 16809 pc2dvds 16811 pockthlem 16837 ablfacrplem 19977 znrrg 21428 opnfbas 23668 supfil 23721 itg1addlem4 25550 itg1addlem4OLD 25551 itg1addlem5 25552 mpodvdsmulf1o 27042 dvdsmulf1o 27044 ppiub 27053 dchrelbas4 27092 2sqlem8 27275 tgldimor 28222 subfacp1lem6 34665 cvmsss2 34754 ax6e2ndeq 43809 supminfxr2 44664 fourierdlem56 45363 ichnreuop 46625 |
Copyright terms: Public domain | W3C validator |