![]() |
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 2824 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon1bi.1 | . . 3 ⊢ (𝐴 ≠ 𝐵 → 𝜑) | |
3 | 1, 2 | sylbir 225 | . 2 ⊢ (¬ 𝐴 = 𝐵 → 𝜑) |
4 | 3 | con1i 144 | 1 ⊢ (¬ 𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1523 ≠ wne 2823 |
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 197 df-ne 2824 |
This theorem is referenced by: necon4ai 2854 fvbr0 6253 peano5 7131 1stnpr 7214 2ndnpr 7215 1st2val 7238 2nd2val 7239 eceqoveq 7895 mapprc 7903 ixp0 7983 setind 8648 hashfun 13262 hashf1lem2 13278 iswrdi 13341 dvdsrval 18691 thlle 20089 konigsberg 27235 hatomistici 29349 esumrnmpt2 30258 mppsval 31595 setindtr 37908 fourierdlem72 40713 afvpcfv0 41547 |
Copyright terms: Public domain | W3C validator |