![]() |
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 2944 | . . 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 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: pm2.61ne 3027 pm2.61dne 3028 pm2.61iine 3032 raaan 4479 raaanv 4480 iinrab2 5031 iinvdif 5041 riinrab 5045 reusv2lem2 5355 po2ne 5562 xpriindi 5793 dmxpid 5886 dmxpss 6124 rnxpid 6126 cnvpo 6240 xpcoid 6243 dfpo2 6249 fnprb 7159 fntpb 7160 xpexr 7856 frxp 8059 suppimacnv 8106 fodomr 9075 wdompwdom 9519 en3lp 9555 inf3lemd 9568 prdom2 9947 iunfictbso 10055 infpssrlem4 10247 1re 11160 dedekindle 11324 00id 11335 nn0lt2 12571 nn01to3 12871 ioorebas 13374 fzfi 13883 ssnn0fi 13896 hash2prde 14375 repswsymballbi 14674 cshw0 14688 cshwmodn 14689 cshwsublen 14690 cshwn 14691 cshwlen 14693 cshwidx0 14700 dmtrclfv 14909 cncongr2 16549 cshwsidrepswmod0 16972 cshwshashlem1 16973 cshwshashlem2 16974 cshwsdisj 16976 cntzssv 19113 psgnunilem4 19284 sdrgacs 20282 mulmarep1gsum2 21939 plyssc 25577 cxpsqrtth 26100 addsqnreup 26807 2sqreultlem 26811 2sqreunnltlem 26814 noresle 27061 axsegcon 27918 axpaschlem 27931 axlowdimlem16 27948 axcontlem7 27961 axcontlem8 27962 axcontlem12 27966 umgrislfupgrlem 28115 edglnl 28136 uhgr2edg 28198 1egrvtxdg0 28501 uspgrn2crct 28795 2pthon3v 28930 clwwlknon0 29079 1pthon2v 29139 1to3vfriswmgr 29266 frgrnbnb 29279 numclwwlk5 29374 siii 29837 h1de2ctlem 30539 riesz3i 31046 unierri 31088 dya2iocuni 32940 sibf0 32991 bnj1143 33459 bnj571 33575 bnj594 33581 bnj852 33590 cgrextend 34639 ifscgr 34675 idinside 34715 btwnconn1lem12 34729 btwnconn1 34732 linethru 34784 bj-xpnzex 35476 ovoliunnfl 36166 voliunnfl 36168 volsupnfl 36169 sn-1ne2 40824 cantnfresb 41702 ax6e2ndeq 42929 lighneal 45889 nrhmzr 46257 zlmodzxznm 46664 itsclc0yqe 46933 |
Copyright terms: Public domain | W3C validator |