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 3032 | . 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓)) |
3 | notnotr 132 | . 2 ⊢ (¬ ¬ 𝜓 → 𝜓) | |
4 | 2, 3 | syl6 35 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ≠ wne 3016 |
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 208 df-ne 3017 |
This theorem is referenced by: om00 8191 pw2f1olem 8610 xlt2add 12643 hashfun 13788 hashtpg 13833 fsumcl2lem 15078 fprodcl2lem 15294 gcdeq0 15855 lcmeq0 15934 lcmfeq0b 15964 phibndlem 16097 abvn0b 20005 cfinufil 22466 isxmet2d 22866 i1fres 24235 tdeglem4 24583 ply1domn 24646 pilem2 24969 isnsqf 25640 ppieq0 25681 chpeq0 25712 chteq0 25713 ltrnatlw 37201 bcc0 40552 |
Copyright terms: Public domain | W3C validator |