![]() |
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 2981 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 = wceq 1542 ≠ wne 2940 |
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 206 df-ne 2941 |
This theorem is referenced by: necon4bid 2986 omwordi 8519 omass 8528 nnmwordi 8583 sdom1OLD 9190 pceq0 16748 f1otrspeq 19234 pmtrfinv 19248 symggen 19257 psgnunilem1 19280 mdetralt 21973 mdetunilem7 21983 ftalem5 26442 fsumvma 26577 dchrelbas4 26607 nosepssdm 27050 fvdifsupp 31645 creq0 31699 fsumcvg4 32588 lkreqN 37678 flt4lem5elem 41032 |
Copyright terms: Public domain | W3C validator |