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 2827 | . 2 ⊢ (𝜑 → 𝐵 = 𝐴) |
3 | eqnetrrd.2 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐶) | |
4 | 2, 3 | eqnetrd 3083 | 1 ⊢ (𝜑 → 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ≠ wne 3016 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-ne 3017 |
This theorem is referenced by: eqnetrrid 3091 3netr3d 3092 cantnflem1c 9139 eqsqrt2d 14718 tanval2 15476 tanval3 15477 tanhlt1 15503 pcadd 16215 efgsres 18795 gsumval3 18958 ablfac 19141 ablsimpgfind 19163 isdrngrd 19459 lspsneq 19825 lebnumlem3 23496 minveclem4a 23962 evthicc 23989 ioorf 24103 deg1ldgn 24616 fta1blem 24691 vieta1lem1 24828 vieta1lem2 24829 vieta1 24830 tanregt0 25050 isosctrlem2 25324 angpieqvd 25336 chordthmlem2 25338 dcubic2 25349 dquartlem1 25356 dquart 25358 asinlem 25373 atandmcj 25414 2efiatan 25423 tanatan 25424 dvatan 25440 dmgmn0 25531 dmgmdivn0 25533 lgamgulmlem2 25535 gamne0 25551 footexALT 26432 footexlem1 26433 footexlem2 26434 ttgcontlem1 26599 wlkn0 27330 fsuppcurry1 30388 fsuppcurry2 30389 bcm1n 30445 sibfof 31498 nosep1o 33084 noetalem3 33117 finxpreclem2 34554 poimirlem9 34783 heicant 34809 heiborlem6 34977 lkrlspeqN 36189 cdlemg18d 37699 cdlemg21 37704 dibord 38177 lclkrlem2u 38545 lcfrlem9 38568 mapdindp4 38741 hdmaprnlem3uN 38869 hdmaprnlem9N 38875 binomcxplemnotnn0 40568 dstregt0 41427 stoweidlem31 42197 stoweidlem59 42225 wallispilem4 42234 dirkertrigeqlem2 42265 fourierdlem43 42316 fourierdlem65 42337 |
Copyright terms: Public domain | W3C validator |