|   | 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 2958 | . 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 = 𝐵)) | 
| 4 | 1, 3 | syl5 34 | 1 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ≠ wne 2940 | 
| 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 2941 | 
| This theorem is referenced by: necon1d 2962 fisseneq 9293 f1finf1o 9305 f1finf1oOLD 9306 dfac5 10169 isf32lem9 10401 fpwwe2 10683 qextlt 13245 qextle 13246 xsubge0 13303 hashf1 14496 climuni 15588 rpnnen2lem12 16261 fzo0dvdseq 16360 4sqlem11 16993 haust1 23360 deg1lt0 26130 ply1divmo 26175 ig1peu 26214 dgrlt 26306 quotcan 26351 fta 27123 atcv0eq 32398 erdszelem9 35204 poimirlem23 37650 poimir 37660 lshpdisj 38988 lsatcv0eq 39048 exatleN 39406 atcvr0eq 39428 cdlemg31c 40701 itrere 42353 sn-itrere 42498 sn-retire 42499 jm2.19 43005 jm2.26lem3 43013 dgraa0p 43161 | 
| Copyright terms: Public domain | W3C validator |