|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > necon3bi | Structured version Visualization version GIF version | ||
| Description: Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) | 
| Ref | Expression | 
|---|---|
| necon3bi.1 | ⊢ (𝐴 = 𝐵 → 𝜑) | 
| Ref | Expression | 
|---|---|
| necon3bi | ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | necon3bi.1 | . . 3 ⊢ (𝐴 = 𝐵 → 𝜑) | |
| 2 | 1 | con3i 154 | . 2 ⊢ (¬ 𝜑 → ¬ 𝐴 = 𝐵) | 
| 3 | 2 | neqned 2946 | 1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1539 ≠ wne 2939 | 
| 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 207 df-ne 2940 | 
| This theorem is referenced by: r19.2zb 4495 pwne 5352 alephord 10116 ackbij1lem18 10277 fin23lem26 10366 fin1a2lem6 10446 alephom 10626 gchxpidm 10710 egt2lt3 16243 nn0onn 16418 prmodvdslcmf 17086 symgfix2 19435 alexsubALTlem2 24057 alexsubALTlem4 24059 ptcmplem2 24062 nmoid 24764 cxplogb 26830 axlowdimlem17 28974 frgrncvvdeq 30329 hashxpe 32812 hasheuni 34087 limsucncmpi 36447 matunitlindflem1 37624 poimirlem32 37660 ovoliunnfl 37670 voliunnfl 37672 volsupnfl 37673 dvasin 37712 lsat0cv 39035 unitscyglem4 42200 metakunt24 42230 readvrec2 42396 readvrec 42397 pellexlem5 42849 uzfissfz 45342 xralrple2 45370 infxr 45383 icccncfext 45907 ioodvbdlimc1lem1 45951 volioc 45992 fourierdlem32 46159 fourierdlem49 46175 fourierdlem73 46199 fourierswlem 46250 fouriersw 46251 sge0pr 46414 voliunsge0lem 46492 carageniuncl 46543 isomenndlem 46550 hoimbl 46651 | 
| Copyright terms: Public domain | W3C validator |