![]() |
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 2985 | . 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓)) |
3 | notnotr 128 | . 2 ⊢ (¬ ¬ 𝜓 → 𝜓) | |
4 | 2, 3 | syl6 35 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1601 ≠ wne 2969 |
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 2970 |
This theorem is referenced by: om00 7939 pw2f1olem 8352 xlt2add 12402 hashfun 13538 hashtpg 13581 fsumcl2lem 14869 fprodcl2lem 15083 gcdeq0 15644 lcmeq0 15719 lcmfeq0b 15749 phibndlem 15879 abvn0b 19699 cfinufil 22140 isxmet2d 22540 i1fres 23909 tdeglem4 24257 ply1domn 24320 pilem2 24643 isnsqf 25313 ppieq0 25354 chpeq0 25385 chteq0 25386 ltrnatlw 36337 bcc0 39495 |
Copyright terms: Public domain | W3C validator |