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 2950 | 1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1539 ≠ wne 2943 |
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 2944 |
This theorem is referenced by: r19.2zb 4426 pwne 5273 onnevOLD 6388 alephord 9831 ackbij1lem18 9993 fin23lem26 10081 fin1a2lem6 10161 alephom 10341 gchxpidm 10425 egt2lt3 15915 nn0onn 16089 prmodvdslcmf 16748 symgfix2 19024 alexsubALTlem2 23199 alexsubALTlem4 23201 ptcmplem2 23204 nmoid 23906 cxplogb 25936 axlowdimlem17 27326 frgrncvvdeq 28673 hashxpe 31127 hasheuni 32053 limsucncmpi 34634 matunitlindflem1 35773 poimirlem32 35809 ovoliunnfl 35819 voliunnfl 35821 volsupnfl 35822 dvasin 35861 lsat0cv 37047 metakunt24 40148 pellexlem5 40655 uzfissfz 42865 xralrple2 42893 infxr 42906 icccncfext 43428 ioodvbdlimc1lem1 43472 volioc 43513 fourierdlem32 43680 fourierdlem49 43696 fourierdlem73 43720 fourierswlem 43771 fouriersw 43772 sge0pr 43932 voliunsge0lem 44010 carageniuncl 44061 isomenndlem 44068 hoimbl 44169 |
Copyright terms: Public domain | W3C validator |