![]() |
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 2945 | . 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓)) |
3 | notnotr 130 | . 2 ⊢ (¬ ¬ 𝜓 → 𝜓) | |
4 | 2, 3 | syl6 35 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1533 ≠ wne 2929 |
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 2930 |
This theorem is referenced by: om00 8596 pw2f1olem 9101 xlt2add 13274 hashfun 14432 hashtpg 14482 fsumcl2lem 15713 fprodcl2lem 15930 gcdeq0 16495 lcmeq0 16574 lcmfeq0b 16604 phibndlem 16742 abvn0b 21269 cfinufil 23876 isxmet2d 24277 i1fres 25679 tdeglem4 26039 tdeglem4OLD 26040 ply1domn 26104 pilem2 26434 isnsqf 27112 ppieq0 27153 chpeq0 27186 chteq0 27187 ltrnatlw 39783 bcc0 43916 |
Copyright terms: Public domain | W3C validator |