Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon1bi | Structured version Visualization version GIF version |
Description: Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
Ref | Expression |
---|---|
necon1bi.1 | ⊢ (𝐴 ≠ 𝐵 → 𝜑) |
Ref | Expression |
---|---|
necon1bi | ⊢ (¬ 𝜑 → 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 3017 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon1bi.1 | . . 3 ⊢ (𝐴 ≠ 𝐵 → 𝜑) | |
3 | 1, 2 | sylbir 236 | . 2 ⊢ (¬ 𝐴 = 𝐵 → 𝜑) |
4 | 3 | con1i 149 | 1 ⊢ (¬ 𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = 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: necon4ai 3047 fvbr0 6691 peano5 7593 1stnpr 7684 2ndnpr 7685 1st2val 7708 2nd2val 7709 eceqoveq 8392 mapprc 8400 ixp0 8484 setind 9165 hashfun 13788 hashf1lem2 13804 iswrdi 13855 ffz0iswrd 13881 dvdsrval 19326 thlle 20771 konigsberg 27964 hatomistici 30067 esumrnmpt2 31227 mppsval 32717 setindtr 39501 fourierdlem72 42344 afvpcfv0 43226 |
Copyright terms: Public domain | W3C validator |