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 2949 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) | |
2 | necon3ai.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
3 | 1, 2 | nsyl 140 | 1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1539 ≠ wne 2943 |
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 2944 |
This theorem is referenced by: necon1ai 2971 necon3i 2976 neneor 3044 nelsn 4601 disjsn2 4648 prnesn 4790 opelopabsb 5443 funsndifnop 7023 ord1eln01 8326 map0b 8671 mapdom3 8936 cflim2 10019 isfin4p1 10071 fpwwe2lem12 10398 tskuni 10539 recextlem2 11606 hashprg 14110 eqsqrt2d 15080 gcd1 16235 gcdzeq 16262 lcmfunsnlem2lem1 16343 lcmfunsnlem2lem2 16344 phimullem 16480 pcgcd1 16578 pc2dvds 16580 pockthlem 16606 ablfacrplem 19668 znrrg 20773 opnfbas 22993 supfil 23046 itg1addlem4 24863 itg1addlem4OLD 24864 itg1addlem5 24865 dvdsmulf1o 26343 ppiub 26352 dchrelbas4 26391 2sqlem8 26574 tgldimor 26863 subfacp1lem6 33147 cvmsss2 33236 ax6e2ndeq 42179 supminfxr2 43009 fourierdlem56 43703 ichnreuop 44924 |
Copyright terms: Public domain | W3C validator |