|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > necon4bd | Structured version Visualization version GIF version | ||
| Description: Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) | 
| Ref | Expression | 
|---|---|
| necon4bd.1 | ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) | 
| Ref | Expression | 
|---|---|
| necon4bd | ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | necon4bd.1 | . . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) | |
| 2 | 1 | necon2bd 2956 | . 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓)) | 
| 3 | notnotr 130 | . 2 ⊢ (¬ ¬ 𝜓 → 𝜓) | |
| 4 | 2, 3 | syl6 35 | 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: iftrueb 4538 om00 8613 pw2f1olem 9116 xlt2add 13302 hashfun 14476 hashtpg 14524 fsumcl2lem 15767 fprodcl2lem 15986 gcdeq0 16554 lcmeq0 16637 lcmfeq0b 16667 phibndlem 16807 abvn0b 20837 cfinufil 23936 isxmet2d 24337 i1fres 25740 tdeglem4 26099 ply1domn 26163 pilem2 26496 isnsqf 27178 ppieq0 27219 chpeq0 27252 chteq0 27253 ltrnatlw 40185 bcc0 44359 | 
| Copyright terms: Public domain | W3C validator |