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 2982 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓)) |
4 | 1, 3 | bitr4id 290 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 = wceq 1542 ≠ wne 2945 |
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 2946 |
This theorem is referenced by: sossfld 6088 fin23lem24 10079 isf32lem4 10113 sqgt0sr 10863 leltne 11065 xrleltne 12878 xrltne 12896 ge0nemnf 12906 xlt2add 12993 supxrbnd 13061 supxrre2 13064 ioopnfsup 13582 icopnfsup 13583 xblpnfps 23546 xblpnf 23547 nmoreltpnf 29127 nmopreltpnf 30227 funeldmb 33733 elprneb 44491 |
Copyright terms: Public domain | W3C validator |