![]() |
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 2977 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓)) |
4 | 1, 3 | bitr4id 289 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 = wceq 1541 ≠ 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 6185 funeldmb 7358 fin23lem24 10319 isf32lem4 10353 sqgt0sr 11103 leltne 11305 xrleltne 13126 xrltne 13144 ge0nemnf 13154 xlt2add 13241 supxrbnd 13309 supxrre2 13312 ioopnfsup 13831 icopnfsup 13832 xblpnfps 23908 xblpnf 23909 nmoreltpnf 30060 nmopreltpnf 31160 elprneb 45818 |
Copyright terms: Public domain | W3C validator |