![]() |
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 2933 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon1bi.1 | . . 3 ⊢ (𝐴 ≠ 𝐵 → 𝜑) | |
3 | 1, 2 | sylbir 234 | . 2 ⊢ (¬ 𝐴 = 𝐵 → 𝜑) |
4 | 3 | con1i 147 | 1 ⊢ (¬ 𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1533 ≠ wne 2932 |
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 2933 |
This theorem is referenced by: necon4ai 2964 iotanul2 6503 fvbr0 6910 peano5 7877 peano5OLD 7878 1stnpr 7972 2ndnpr 7973 1st2val 7996 2nd2val 7997 eceqoveq 8811 mapprc 8819 ixp0 8920 cnvfi 9175 setind 9724 hashfun 14393 hashf1lem2 14413 iswrdi 14464 ffz0iswrd 14487 dvdsrval 20248 thlle 21551 thlleOLD 21552 konigsberg 29934 hatomistici 32039 esumrnmpt2 33521 mppsval 35018 setindtr 42218 fourierdlem72 45345 afvpcfv0 46305 |
Copyright terms: Public domain | W3C validator |