|   | 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 2980 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 = wceq 1539 ≠ 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 207 df-ne 2940 | 
| This theorem is referenced by: necon4bid 2985 fvdifsupp 8197 omwordi 8610 omass 8619 nnmwordi 8674 sdom1OLD 9280 pceq0 16910 f1otrspeq 19466 pmtrfinv 19480 symggen 19489 psgnunilem1 19512 mdetralt 22615 mdetunilem7 22625 ftalem5 27121 fsumvma 27258 dchrelbas4 27288 nosepssdm 27732 creq0 32747 fsumcvg4 33950 lkreqN 39172 flt4lem5elem 42666 | 
| Copyright terms: Public domain | W3C validator |