![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqnetrrd | Structured version Visualization version GIF version |
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
Ref | Expression |
---|---|
eqnetrrd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
eqnetrrd.2 | ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Ref | Expression |
---|---|
eqnetrrd | ⊢ (𝜑 → 𝐵 ≠ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqnetrrd.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | eqcomd 2777 | . 2 ⊢ (𝜑 → 𝐵 = 𝐴) |
3 | eqnetrrd.2 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐶) | |
4 | 2, 3 | eqnetrd 3027 | 1 ⊢ (𝜑 → 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1508 ≠ wne 2960 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-9 2060 ax-ext 2743 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1744 df-cleq 2764 df-ne 2961 |
This theorem is referenced by: syl5eqner 3035 3netr3d 3036 cantnflem1c 8942 eqsqrt2d 14587 tanval2 15344 tanval3 15345 tanhlt1 15371 pcadd 16079 efgsres 18634 efgsresOLD 18635 gsumval3 18793 ablfac 18972 isdrngrd 19263 lspsneq 19628 lebnumlem3 23285 minveclem4a 23751 evthicc 23778 ioorf 23892 deg1ldgn 24405 fta1blem 24480 vieta1lem1 24617 vieta1lem2 24618 vieta1 24619 tanregt0 24839 isosctrlem2 25113 angpieqvd 25125 chordthmlem2 25127 dcubic2 25138 dquartlem1 25145 dquart 25147 asinlem 25162 atandmcj 25203 2efiatan 25212 tanatan 25213 dvatan 25229 dmgmn0 25320 dmgmdivn0 25322 lgamgulmlem2 25324 gamne0 25340 footexALT 26221 footexlem1 26222 footexlem2 26223 ttgcontlem1 26389 wlkn0 27120 fsuppcurry1 30237 fsuppcurry2 30238 bcm1n 30291 sibfof 31275 nosep1o 32744 noetalem3 32777 finxpreclem2 34149 poimirlem9 34379 heicant 34405 heiborlem6 34573 lkrlspeqN 35789 cdlemg18d 37299 cdlemg21 37304 dibord 37777 lclkrlem2u 38145 lcfrlem9 38168 mapdindp4 38341 hdmaprnlem3uN 38469 hdmaprnlem9N 38475 ablsimpgfind 40083 binomcxplemnotnn0 40142 dstregt0 41008 stoweidlem31 41779 stoweidlem59 41807 wallispilem4 41816 dirkertrigeqlem2 41847 fourierdlem43 41898 fourierdlem65 41919 |
Copyright terms: Public domain | W3C validator |