|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > necon4ad | Structured version Visualization version GIF version | ||
| Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) | 
| Ref | Expression | 
|---|---|
| necon4ad.1 | ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) | 
| Ref | Expression | 
|---|---|
| necon4ad | ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | notnot 142 | . 2 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
| 2 | necon4ad.1 | . . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) | |
| 3 | 2 | necon1bd 2957 | . 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 = 𝐵)) | 
| 4 | 1, 3 | syl5 34 | 1 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1539 ≠ wne 2939 | 
| 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 207 df-ne 2940 | 
| This theorem is referenced by: necon1d 2961 fisseneq 9294 f1finf1o 9306 f1finf1oOLD 9307 dfac5 10170 isf32lem9 10402 fpwwe2 10684 qextlt 13246 qextle 13247 xsubge0 13304 hashf1 14497 climuni 15589 rpnnen2lem12 16262 fzo0dvdseq 16361 4sqlem11 16994 haust1 23361 deg1lt0 26131 ply1divmo 26176 ig1peu 26215 dgrlt 26307 quotcan 26352 fta 27124 atcv0eq 32399 erdszelem9 35205 poimirlem23 37651 poimir 37661 lshpdisj 38989 lsatcv0eq 39049 exatleN 39407 atcvr0eq 39429 cdlemg31c 40702 itrere 42358 sn-itrere 42503 sn-retire 42504 jm2.19 43010 jm2.26lem3 43018 dgraa0p 43166 | 
| Copyright terms: Public domain | W3C validator |