![]() |
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 314 | . 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓) | |
2 | necon2abid.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) | |
3 | 2 | necon3abid 2967 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓)) |
4 | 1, 3 | bitr4id 289 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 = wceq 1534 ≠ wne 2930 |
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 2931 |
This theorem is referenced by: sossfld 6197 funeldmb 7371 fin23lem24 10365 isf32lem4 10399 sqgt0sr 11149 leltne 11353 xrleltne 13178 xrltne 13196 ge0nemnf 13206 xlt2add 13293 supxrbnd 13361 supxrre2 13364 ioopnfsup 13884 icopnfsup 13885 xblpnfps 24392 xblpnf 24393 nmoreltpnf 30702 nmopreltpnf 31802 elprneb 46644 |
Copyright terms: Public domain | W3C validator |