| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > necon2abid | Structured version Visualization version GIF version | ||
| Description: Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
| Ref | Expression |
|---|---|
| necon2abid.1 | ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) |
| Ref | Expression |
|---|---|
| necon2abid | ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | notnotb 315 | . 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓) | |
| 2 | necon2abid.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) | |
| 3 | 2 | necon3abid 2977 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓)) |
| 4 | 1, 3 | bitr4id 290 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 = wceq 1540 ≠ 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 207 df-ne 2941 |
| This theorem is referenced by: sossfld 6206 funeldmb 7379 fin23lem24 10362 isf32lem4 10396 sqgt0sr 11146 leltne 11350 xrleltne 13187 xrltne 13205 ge0nemnf 13215 xlt2add 13302 supxrbnd 13370 supxrre2 13373 ioopnfsup 13904 icopnfsup 13905 xblpnfps 24405 xblpnf 24406 nmoreltpnf 30788 nmopreltpnf 31888 elprneb 47041 |
| Copyright terms: Public domain | W3C validator |