![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.61ine | Structured version Visualization version GIF version |
Description: Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
pm2.61ine.1 | ⊢ (𝐴 = 𝐵 → 𝜑) |
pm2.61ine.2 | ⊢ (𝐴 ≠ 𝐵 → 𝜑) |
Ref | Expression |
---|---|
pm2.61ine | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.61ine.2 | . 2 ⊢ (𝐴 ≠ 𝐵 → 𝜑) | |
2 | nne 2936 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
3 | pm2.61ine.1 | . . 3 ⊢ (𝐴 = 𝐵 → 𝜑) | |
4 | 2, 3 | sylbi 207 | . 2 ⊢ (¬ 𝐴 ≠ 𝐵 → 𝜑) |
5 | 1, 4 | pm2.61i 176 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1632 ≠ 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 197 df-ne 2933 |
This theorem is referenced by: pm2.61ne 3017 pm2.61iine 3022 rgenzOLD 4221 raaan 4226 iinrab2 4735 iinvdif 4744 riinrab 4748 reusv2lem2 5018 reusv2lem2OLD 5019 xpriindi 5414 dmxpid 5500 dmxpss 5723 rnxpid 5725 cnvpo 5834 xpcoid 5837 fnprb 6636 fntpb 6637 xpexr 7271 frxp 7455 suppimacnv 7474 fodomr 8276 wdompwdom 8648 en3lp 8682 inf3lemd 8697 prdom2 9019 iunfictbso 9127 infpssrlem4 9320 1re 10231 dedekindle 10393 00id 10403 nn0lt2 11632 nn01to3 11974 ioorebas 12468 fzfi 12965 ssnn0fi 12978 hash2prde 13444 repswsymballbi 13727 cshw0 13740 cshwmodn 13741 cshwsublen 13742 cshwn 13743 cshwlen 13745 cshwidx0 13752 dmtrclfv 13958 cncongr2 15584 cshwsidrepswmod0 16003 cshwshashlem1 16004 cshwshashlem2 16005 cshwsdisj 16007 cntzssv 17961 psgnunilem4 18117 mulmarep1gsum2 20582 plyssc 24155 axsegcon 26006 axpaschlem 26019 axlowdimlem16 26036 axcontlem7 26049 axcontlem8 26050 axcontlem12 26054 umgrislfupgrlem 26216 edglnl 26237 uhgr2edg 26299 1egrvtxdg0 26617 uspgrn2crct 26911 2pthon3v 27063 clwwlknon0 27240 1pthon2v 27305 1to3vfriswmgr 27434 frgrnbnb 27447 numclwwlk5 27556 siii 28017 h1de2ctlem 28723 riesz3i 29230 unierri 29272 dya2iocuni 30654 sibf0 30705 bnj1143 31168 bnj571 31283 bnj594 31289 bnj852 31298 dfpo2 31952 noresle 32152 cgrextend 32421 ifscgr 32457 idinside 32497 btwnconn1lem12 32511 btwnconn1 32514 linethru 32566 bj-xpnzex 33252 ovoliunnfl 33764 voliunnfl 33766 volsupnfl 33767 sdrgacs 38273 ax6e2ndeq 39277 lighneal 42038 nrhmzr 42383 zlmodzxznm 42796 |
Copyright terms: Public domain | W3C validator |