![]() |
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 2943 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
3 | pm2.61ine.1 | . . 3 ⊢ (𝐴 = 𝐵 → 𝜑) | |
4 | 2, 3 | sylbi 216 | . 2 ⊢ (¬ 𝐴 ≠ 𝐵 → 𝜑) |
5 | 1, 4 | pm2.61i 182 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ≠ 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 206 df-ne 2940 |
This theorem is referenced by: pm2.61ne 3026 pm2.61dne 3027 pm2.61iine 3031 raaan 4520 raaanv 4521 iinrab2 5073 iinvdif 5083 riinrab 5087 reusv2lem2 5397 po2ne 5604 xpriindi 5836 dmxpid 5929 dmxpss 6170 rnxpid 6172 cnvpo 6286 xpcoid 6289 dfpo2 6295 fnprb 7212 fntpb 7213 xpexr 7913 frxp 8117 suppimacnv 8164 fodomr 9134 wdompwdom 9579 en3lp 9615 inf3lemd 9628 prdom2 10007 iunfictbso 10115 infpssrlem4 10307 1re 11221 dedekindle 11385 00id 11396 nn0lt2 12632 nn01to3 12932 ioorebas 13435 fzfi 13944 ssnn0fi 13957 hash2prde 14438 repswsymballbi 14737 cshw0 14751 cshwmodn 14752 cshwsublen 14753 cshwn 14754 cshwlen 14756 cshwidx0 14763 dmtrclfv 14972 cncongr2 16612 cshwsidrepswmod0 17035 cshwshashlem1 17036 cshwshashlem2 17037 cshwsdisj 17039 cntzssv 19240 psgnunilem4 19413 nrhmzr 20433 sdrgacs 20648 mulmarep1gsum2 22397 plyssc 26053 cxpsqrtth 26579 addsqnreup 27291 2sqreultlem 27295 2sqreunnltlem 27298 noresle 27545 axsegcon 28620 axpaschlem 28633 axlowdimlem16 28650 axcontlem7 28663 axcontlem8 28664 axcontlem12 28668 umgrislfupgrlem 28817 edglnl 28838 uhgr2edg 28900 1egrvtxdg0 29203 uspgrn2crct 29497 2pthon3v 29632 clwwlknon0 29781 1pthon2v 29841 1to3vfriswmgr 29968 frgrnbnb 29981 numclwwlk5 30076 siii 30541 h1de2ctlem 31243 riesz3i 31750 unierri 31792 dya2iocuni 33748 sibf0 33799 bnj1143 34267 bnj571 34383 bnj594 34389 bnj852 34398 cgrextend 35452 ifscgr 35488 idinside 35528 btwnconn1lem12 35542 btwnconn1 35545 linethru 35597 bj-xpnzex 36307 ovoliunnfl 36997 voliunnfl 36999 volsupnfl 37000 sn-1ne2 41645 cantnfresb 42540 ax6e2ndeq 43786 lighneal 46741 zlmodzxznm 47343 itsclc0yqe 47612 |
Copyright terms: Public domain | W3C validator |