![]() |
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 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: sossfld 6139 funeldmb 7305 fin23lem24 10263 isf32lem4 10297 sqgt0sr 11047 leltne 11249 xrleltne 13070 xrltne 13088 ge0nemnf 13098 xlt2add 13185 supxrbnd 13253 supxrre2 13256 ioopnfsup 13775 icopnfsup 13776 xblpnfps 23764 xblpnf 23765 nmoreltpnf 29753 nmopreltpnf 30853 elprneb 45349 |
Copyright terms: Public domain | W3C validator |