![]() |
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 3003 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
3 | pm2.61ine.1 | . . 3 ⊢ (𝐴 = 𝐵 → 𝜑) | |
4 | 2, 3 | sylbi 209 | . 2 ⊢ (¬ 𝐴 ≠ 𝐵 → 𝜑) |
5 | 1, 4 | pm2.61i 177 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1656 ≠ wne 2999 |
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 199 df-ne 3000 |
This theorem is referenced by: pm2.61ne 3084 pm2.61iine 3089 raaan 4304 iinrab2 4805 iinvdif 4814 riinrab 4818 reusv2lem2 5101 po2ne 5280 xpriindi 5495 dmxpid 5581 dmxpss 5810 rnxpid 5812 cnvpo 5918 xpcoid 5921 fnprb 6733 fntpb 6734 xpexr 7373 frxp 7556 suppimacnv 7575 fodomr 8386 wdompwdom 8759 en3lp 8793 inf3lemd 8808 prdom2 9149 iunfictbso 9257 infpssrlem4 9450 1re 10363 dedekindle 10527 00id 10537 nn0lt2 11775 nn01to3 12071 ioorebas 12571 fzfi 13073 ssnn0fi 13086 hash2prde 13548 repswsymballbi 13903 cshw0 13922 cshwmodn 13923 cshwsublen 13924 cshwn 13925 cshwlen 13927 cshwidx0 13934 dmtrclfv 14143 cncongr2 15761 cshwsidrepswmod0 16174 cshwshashlem1 16175 cshwshashlem2 16176 cshwsdisj 16178 cntzssv 18118 psgnunilem4 18275 mulmarep1gsum2 20755 plyssc 24362 cxpsqrtth 24881 axsegcon 26233 axpaschlem 26246 axlowdimlem16 26263 axcontlem7 26276 axcontlem8 26277 axcontlem12 26281 umgrislfupgrlem 26427 edglnl 26449 uhgr2edg 26511 1egrvtxdg0 26816 uspgrn2crct 27114 2pthon3v 27279 clwwlknon0 27464 1pthon2v 27525 1to3vfriswmgr 27657 frgrnbnb 27670 numclwwlk5 27799 siii 28259 h1de2ctlem 28965 riesz3i 29472 unierri 29514 dya2iocuni 30886 sibf0 30937 bnj1143 31403 bnj571 31518 bnj594 31524 bnj852 31533 dfpo2 32183 noresle 32380 cgrextend 32649 ifscgr 32685 idinside 32725 btwnconn1lem12 32739 btwnconn1 32742 linethru 32794 bj-xpnzex 33463 ovoliunnfl 33990 voliunnfl 33992 volsupnfl 33993 sdrgacs 38609 ax6e2ndeq 39598 lighneal 42372 nrhmzr 42734 zlmodzxznm 43147 |
Copyright terms: Public domain | W3C validator |