![]() |
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 2936 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
3 | 1, 2 | sylibr 224 | . 2 ⊢ (𝜑 → ¬ 𝐴 ≠ 𝐵) |
4 | 3 | con2i 134 | 1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1632 ≠ 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 197 df-ne 2933 |
This theorem is referenced by: necon1ai 2959 necon3i 2964 neneor 3031 nelsn 4357 disjsn2 4391 prnesn 4538 opelopabsb 5135 0nelxpOLD 5301 funsndifnop 6580 map0b 8064 mapdom3 8299 wemapso2lem 8624 cflim2 9297 isfin4-3 9349 fpwwe2lem13 9676 tskuni 9817 recextlem2 10870 hashprg 13394 hashprgOLD 13395 eqsqrt2d 14327 gcd1 15471 gcdzeq 15493 lcmfunsnlem2lem1 15573 lcmfunsnlem2lem2 15574 phimullem 15706 pcgcd1 15803 pc2dvds 15805 pockthlem 15831 ablfacrplem 18684 znrrg 20136 opnfbas 21867 supfil 21920 itg1addlem4 23685 itg1addlem5 23686 dvdsmulf1o 25140 ppiub 25149 dchrelbas4 25188 lgsne0 25280 2sqlem8 25371 tgldimor 25617 subfacp1lem6 31495 cvmsss2 31584 ax6e2ndeq 39295 supminfxr2 40215 fourierdlem56 40900 |
Copyright terms: Public domain | W3C validator |