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 | notnotb 316 | . . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓) | |
2 | necon2bbid.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) | |
3 | 1, 2 | syl5rbbr 287 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓)) |
4 | 3 | necon4abid 3056 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 = 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: necon4bid 3061 omwordi 8187 omass 8196 nnmwordi 8251 sdom1 8707 pceq0 16197 f1otrspeq 18506 pmtrfinv 18520 symggen 18529 psgnunilem1 18552 mdetralt 21147 mdetunilem7 21157 ftalem5 25582 fsumvma 25717 dchrelbas4 25747 creq0 30398 fsumcvg4 31093 nosepssdm 33088 lkreqN 36188 |
Copyright terms: Public domain | W3C validator |