![]() |
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 2947 | 1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ≠ wne 2940 |
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 2941 |
This theorem is referenced by: r19.2zb 4457 pwne 5311 onnevOLD 6449 alephord 10019 ackbij1lem18 10181 fin23lem26 10269 fin1a2lem6 10349 alephom 10529 gchxpidm 10613 egt2lt3 16096 nn0onn 16270 prmodvdslcmf 16927 symgfix2 19206 alexsubALTlem2 23422 alexsubALTlem4 23424 ptcmplem2 23427 nmoid 24129 cxplogb 26159 axlowdimlem17 27956 frgrncvvdeq 29302 hashxpe 31765 hasheuni 32748 limsucncmpi 34970 matunitlindflem1 36124 poimirlem32 36160 ovoliunnfl 36170 voliunnfl 36172 volsupnfl 36173 dvasin 36212 lsat0cv 37545 metakunt24 40650 pellexlem5 41203 uzfissfz 43651 xralrple2 43679 infxr 43692 icccncfext 44218 ioodvbdlimc1lem1 44262 volioc 44303 fourierdlem32 44470 fourierdlem49 44486 fourierdlem73 44510 fourierswlem 44561 fouriersw 44562 sge0pr 44725 voliunsge0lem 44803 carageniuncl 44854 isomenndlem 44861 hoimbl 44962 |
Copyright terms: Public domain | W3C validator |