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 | necon2abid.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓)) | |
2 | 1 | necon3abid 3052 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓)) |
3 | notnotb 316 | . 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓) | |
4 | 2, 3 | syl6rbbr 291 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 = wceq 1528 ≠ wne 3016 |
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 208 df-ne 3017 |
This theorem is referenced by: sossfld 6037 fin23lem24 9733 isf32lem4 9767 sqgt0sr 10517 leltne 10719 xrleltne 12528 xrltne 12546 ge0nemnf 12556 xlt2add 12643 supxrbnd 12711 supxrre2 12714 ioopnfsup 13222 icopnfsup 13223 xblpnfps 22934 xblpnf 22935 nmoreltpnf 28474 nmopreltpnf 29574 funeldmb 32904 elprneb 43145 |
Copyright terms: Public domain | W3C validator |