![]() |
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 2742 | . 2 ⊢ (𝜑 → 𝐵 = 𝐴) |
3 | eqnetrrd.2 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐶) | |
4 | 2, 3 | eqnetrd 3009 | 1 ⊢ (𝜑 → 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ≠ wne 2941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2728 df-ne 2942 |
This theorem is referenced by: eqnetrrid 3017 3netr3d 3018 cantnflem1c 9619 eqsqrt2d 15245 tanval2 16007 tanval3 16008 tanhlt1 16034 pcadd 16753 efgsres 19511 gsumval3 19675 ablfac 19858 ablsimpgfind 19880 isdrngrd 20200 lspsneq 20568 lebnumlem3 24310 minveclem4a 24778 evthicc 24807 ioorf 24921 deg1ldgn 25442 fta1blem 25517 vieta1lem1 25654 vieta1lem2 25655 vieta1 25656 tanregt0 25879 isosctrlem2 26153 angpieqvd 26165 chordthmlem2 26167 dcubic2 26178 dquartlem1 26185 dquart 26187 asinlem 26202 atandmcj 26243 2efiatan 26252 tanatan 26253 dvatan 26269 dmgmn0 26359 dmgmdivn0 26361 lgamgulmlem2 26363 gamne0 26379 nosep1o 27013 noetasuplem4 27068 footexALT 27546 footexlem1 27547 footexlem2 27548 ttgcontlem1 27719 wlkn0 28455 fsuppcurry1 31525 fsuppcurry2 31526 bcm1n 31581 zarclssn 32323 sibfof 32809 finxpreclem2 35828 poimirlem9 36054 heicant 36080 heiborlem6 36242 lkrlspeqN 37600 cdlemg18d 39111 cdlemg21 39116 dibord 39589 lclkrlem2u 39957 lcfrlem9 39980 mapdindp4 40153 hdmaprnlem3uN 40281 hdmaprnlem9N 40287 fsuppind 40703 binomcxplemnotnn0 42578 dstregt0 43451 stoweidlem31 44204 stoweidlem59 44232 wallispilem4 44241 dirkertrigeqlem2 44272 fourierdlem43 44323 fourierdlem65 44344 catprs 46963 |
Copyright terms: Public domain | W3C validator |