![]() |
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 3008 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓)) |
3 | notnotb 307 | . 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓) | |
4 | 2, 3 | syl6rbbr 282 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 = wceq 1653 ≠ wne 2972 |
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 199 df-ne 2973 |
This theorem is referenced by: sossfld 5798 fin23lem24 9433 isf32lem4 9467 sqgt0sr 10216 leltne 10418 xrleltne 12224 xrltne 12242 ge0nemnf 12252 xlt2add 12338 supxrbnd 12406 supxrre2 12409 ioopnfsup 12917 icopnfsup 12918 xblpnfps 22527 xblpnf 22528 nmoreltpnf 28148 nmopreltpnf 29252 funeldmb 32174 elprneb 41912 |
Copyright terms: Public domain | W3C validator |