![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon2bbid | Structured version Visualization version GIF version |
Description: Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
Ref | Expression |
---|---|
necon2bbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) |
Ref | Expression |
---|---|
necon2bbid | ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon2bbid.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) | |
2 | notnotb 315 | . . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓) | |
3 | 1, 2 | bitr3di 286 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓)) |
4 | 3 | necon4abid 2979 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 = wceq 1537 ≠ wne 2938 |
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 2939 |
This theorem is referenced by: necon4bid 2984 fvdifsupp 8195 omwordi 8608 omass 8617 nnmwordi 8672 sdom1OLD 9277 pceq0 16905 f1otrspeq 19480 pmtrfinv 19494 symggen 19503 psgnunilem1 19526 mdetralt 22630 mdetunilem7 22640 ftalem5 27135 fsumvma 27272 dchrelbas4 27302 nosepssdm 27746 creq0 32753 fsumcvg4 33911 lkreqN 39152 flt4lem5elem 42638 |
Copyright terms: Public domain | W3C validator |