![]() |
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 3016 | . 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓)) |
3 | notnotr 128 | . 2 ⊢ (¬ ¬ 𝜓 → 𝜓) | |
4 | 2, 3 | syl6 35 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1658 ≠ wne 3000 |
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 199 df-ne 3001 |
This theorem is referenced by: om00 7923 pw2f1olem 8334 xlt2add 12379 hashfun 13514 hashtpg 13557 fsumcl2lem 14840 fprodcl2lem 15054 gcdeq0 15612 lcmeq0 15687 lcmfeq0b 15717 phibndlem 15847 abvn0b 19664 cfinufil 22103 isxmet2d 22503 i1fres 23872 tdeglem4 24220 ply1domn 24283 pilem2 24606 isnsqf 25275 ppieq0 25316 chpeq0 25347 chteq0 25348 ltrnatlw 36259 bcc0 39380 |
Copyright terms: Public domain | W3C validator |