![]() |
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 2766 | . 2 ⊢ (𝜑 → 𝐵 = 𝐴) |
3 | eqnetrrd.2 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐶) | |
4 | 2, 3 | eqnetrd 2999 | 1 ⊢ (𝜑 → 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1632 ≠ wne 2932 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 df-cleq 2753 df-ne 2933 |
This theorem is referenced by: syl5eqner 3007 3netr3d 3008 cantnflem1c 8757 eqsqrt2d 14307 tanval2 15062 tanval3 15063 tanhlt1 15089 pcadd 15795 efgsres 18351 gsumval3 18508 ablfac 18687 isdrngrd 18975 lspsneq 19324 lebnumlem3 22963 minveclem4a 23401 evthicc 23428 ioorf 23541 deg1ldgn 24052 fta1blem 24127 vieta1lem1 24264 vieta1lem2 24265 vieta1 24266 tanregt0 24484 isosctrlem2 24748 angpieqvd 24757 chordthmlem2 24759 dcubic2 24770 dquartlem1 24777 dquart 24779 asinlem 24794 atandmcj 24835 2efiatan 24844 tanatan 24845 dvatan 24861 dmgmn0 24951 dmgmdivn0 24953 lgamgulmlem2 24955 gamne0 24971 footex 25812 ttgcontlem1 25964 wlkn0 26726 bcm1n 29863 sibfof 30711 nosep1o 32138 noetalem3 32171 finxpreclem2 33538 poimirlem9 33731 heicant 33757 heiborlem6 33928 lkrlspeqN 34961 cdlemg18d 36471 cdlemg21 36476 dibord 36950 lclkrlem2u 37318 lcfrlem9 37341 mapdindp4 37514 hdmaprnlem3uN 37645 hdmaprnlem9N 37651 binomcxplemnotnn0 39057 dstregt0 39992 stoweidlem31 40751 stoweidlem59 40779 wallispilem4 40788 dirkertrigeqlem2 40819 fourierdlem43 40870 fourierdlem65 40891 |
Copyright terms: Public domain | W3C validator |