![]() |
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 2978 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓)) |
4 | 1, 3 | bitr4id 290 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 = wceq 1542 ≠ wne 2941 |
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 2942 |
This theorem is referenced by: sossfld 6186 funeldmb 7356 fin23lem24 10317 isf32lem4 10351 sqgt0sr 11101 leltne 11303 xrleltne 13124 xrltne 13142 ge0nemnf 13152 xlt2add 13239 supxrbnd 13307 supxrre2 13310 ioopnfsup 13829 icopnfsup 13830 xblpnfps 23901 xblpnf 23902 nmoreltpnf 30022 nmopreltpnf 31122 elprneb 45739 |
Copyright terms: Public domain | W3C validator |