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 3020 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
3 | pm2.61ine.1 | . . 3 ⊢ (𝐴 = 𝐵 → 𝜑) | |
4 | 2, 3 | sylbi 218 | . 2 ⊢ (¬ 𝐴 ≠ 𝐵 → 𝜑) |
5 | 1, 4 | pm2.61i 183 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ≠ wne 3016 |
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 208 df-ne 3017 |
This theorem is referenced by: pm2.61ne 3102 pm2.61iine 3107 raaan 4458 raaanv 4459 iinrab2 4984 iinvdif 4994 riinrab 4998 reusv2lem2 5291 po2ne 5483 xpriindi 5701 dmxpid 5794 dmxpss 6022 rnxpid 6024 cnvpo 6132 xpcoid 6135 fnprb 6963 fntpb 6964 xpexr 7611 frxp 7811 suppimacnv 7832 fodomr 8657 wdompwdom 9031 en3lp 9066 inf3lemd 9079 prdom2 9421 iunfictbso 9529 infpssrlem4 9717 1re 10630 dedekindle 10793 00id 10804 nn0lt2 12034 nn01to3 12330 ioorebas 12829 fzfi 13330 ssnn0fi 13343 hash2prde 13818 repswsymballbi 14132 cshw0 14146 cshwmodn 14147 cshwsublen 14148 cshwn 14149 cshwlen 14151 cshwidx0 14158 dmtrclfv 14368 cncongr2 16002 cshwsidrepswmod0 16418 cshwshashlem1 16419 cshwshashlem2 16420 cshwsdisj 16422 cntzssv 18398 psgnunilem4 18556 sdrgacs 19511 mulmarep1gsum2 21113 plyssc 24719 cxpsqrtth 25239 addsqnreup 25947 2sqreultlem 25951 2sqreunnltlem 25954 axsegcon 26641 axpaschlem 26654 axlowdimlem16 26671 axcontlem7 26684 axcontlem8 26685 axcontlem12 26689 umgrislfupgrlem 26835 edglnl 26856 uhgr2edg 26918 1egrvtxdg0 27221 uspgrn2crct 27514 2pthon3v 27650 clwwlknon0 27800 1pthon2v 27860 1to3vfriswmgr 27987 frgrnbnb 28000 numclwwlk5 28095 siii 28558 h1de2ctlem 29260 riesz3i 29767 unierri 29809 dya2iocuni 31441 sibf0 31492 bnj1143 31962 bnj571 32078 bnj594 32084 bnj852 32093 dfpo2 32889 noresle 33098 cgrextend 33367 ifscgr 33403 idinside 33443 btwnconn1lem12 33457 btwnconn1 33460 linethru 33512 bj-xpnzex 34169 ovoliunnfl 34816 voliunnfl 34818 volsupnfl 34819 sn-1ne2 39038 ax6e2ndeq 40773 lighneal 43623 nrhmzr 44042 zlmodzxznm 44450 itsclc0yqe 44646 |
Copyright terms: Public domain | W3C validator |