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 2945 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
3 | pm2.61ine.1 | . . 3 ⊢ (𝐴 = 𝐵 → 𝜑) | |
4 | 2, 3 | sylbi 220 | . 2 ⊢ (¬ 𝐴 ≠ 𝐵 → 𝜑) |
5 | 1, 4 | pm2.61i 185 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1543 ≠ wne 2941 |
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 210 df-ne 2942 |
This theorem is referenced by: pm2.61ne 3028 pm2.61dne 3029 pm2.61iine 3033 raaan 4447 raaanv 4448 iinrab2 4993 iinvdif 5003 riinrab 5007 reusv2lem2 5307 po2ne 5499 xpriindi 5720 dmxpid 5814 dmxpss 6049 rnxpid 6051 cnvpo 6165 xpcoid 6168 dfpo2 6174 fnprb 7043 fntpb 7044 xpexr 7715 frxp 7914 suppimacnv 7937 fodomr 8820 wdompwdom 9219 en3lp 9254 inf3lemd 9267 prdom2 9645 iunfictbso 9753 infpssrlem4 9945 1re 10858 dedekindle 11021 00id 11032 nn0lt2 12265 nn01to3 12562 ioorebas 13064 fzfi 13572 ssnn0fi 13585 hash2prde 14064 repswsymballbi 14373 cshw0 14387 cshwmodn 14388 cshwsublen 14389 cshwn 14390 cshwlen 14392 cshwidx0 14399 dmtrclfv 14609 cncongr2 16253 cshwsidrepswmod0 16676 cshwshashlem1 16677 cshwshashlem2 16678 cshwsdisj 16680 cntzssv 18750 psgnunilem4 18917 sdrgacs 19873 mulmarep1gsum2 21498 plyssc 25121 cxpsqrtth 25644 addsqnreup 26351 2sqreultlem 26355 2sqreunnltlem 26358 axsegcon 27045 axpaschlem 27058 axlowdimlem16 27075 axcontlem7 27088 axcontlem8 27089 axcontlem12 27093 umgrislfupgrlem 27240 edglnl 27261 uhgr2edg 27323 1egrvtxdg0 27626 uspgrn2crct 27919 2pthon3v 28054 clwwlknon0 28203 1pthon2v 28263 1to3vfriswmgr 28390 frgrnbnb 28403 numclwwlk5 28498 siii 28961 h1de2ctlem 29663 riesz3i 30170 unierri 30212 dya2iocuni 31989 sibf0 32040 bnj1143 32509 bnj571 32625 bnj594 32631 bnj852 32640 noresle 33666 cgrextend 34076 ifscgr 34112 idinside 34152 btwnconn1lem12 34166 btwnconn1 34169 linethru 34221 bj-xpnzex 34915 ovoliunnfl 35586 voliunnfl 35588 volsupnfl 35589 sn-1ne2 40036 ax6e2ndeq 41885 lighneal 44767 nrhmzr 45135 zlmodzxznm 45542 itsclc0yqe 45811 |
Copyright terms: Public domain | W3C validator |