![]() |
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 314 | . . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓) | |
3 | 1, 2 | bitr3di 285 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓)) |
4 | 3 | necon4abid 2980 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 = wceq 1541 ≠ wne 2939 |
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 2940 |
This theorem is referenced by: necon4bid 2985 omwordi 8554 omass 8563 nnmwordi 8618 sdom1OLD 9226 pceq0 16786 f1otrspeq 19279 pmtrfinv 19293 symggen 19302 psgnunilem1 19325 mdetralt 22039 mdetunilem7 22049 ftalem5 26508 fsumvma 26643 dchrelbas4 26673 nosepssdm 27116 fvdifsupp 31777 creq0 31831 fsumcvg4 32761 lkreqN 37845 flt4lem5elem 41175 |
Copyright terms: Public domain | W3C validator |