![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3netr4d | Structured version Visualization version GIF version |
Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 21-Nov-2019.) |
Ref | Expression |
---|---|
3netr4d.1 | ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
3netr4d.2 | ⊢ (𝜑 → 𝐶 = 𝐴) |
3netr4d.3 | ⊢ (𝜑 → 𝐷 = 𝐵) |
Ref | Expression |
---|---|
3netr4d | ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3netr4d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐴) | |
2 | 3netr4d.1 | . . 3 ⊢ (𝜑 → 𝐴 ≠ 𝐵) | |
3 | 1, 2 | eqnetrd 3008 | . 2 ⊢ (𝜑 → 𝐶 ≠ 𝐵) |
4 | 3netr4d.3 | . 2 ⊢ (𝜑 → 𝐷 = 𝐵) | |
5 | 3, 4 | neeqtrrd 3015 | 1 ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ≠ wne 2940 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 df-ne 2941 |
This theorem is referenced by: infpssrlem4 10247 modsumfzodifsn 13855 mgm2nsgrplem4 18736 pmtr3ncomlem1 19260 isdrng2 20210 prmirredlem 20909 uvcf1 21214 dfac14lem 22984 i1fmullem 25074 fta1glem1 25546 fta1blem 25549 plydivlem4 25672 fta1lem 25683 cubic 26215 asinlem 26234 dchrn0 26614 lgsne0 26699 noextenddif 27032 noresle 27061 perpneq 27698 axlowdimlem14 27946 preimane 31632 cycpmco2lem6 32029 cycpmrn 32041 cntnevol 32884 subfacp1lem5 33835 fvtransport 34663 poimirlem1 36125 poimirlem6 36130 poimirlem7 36131 dalem4 38174 cdleme35sn2aw 38967 cdleme39n 38975 cdleme41fva11 38986 trlcone 39237 hdmaprnlem3N 40359 sticksstones2 40601 uvcn0 40773 flt0 41018 stoweidlem23 44350 2zrngnmlid 46333 2zrngnmrid 46334 zlmodzxznm 46664 line2y 46927 |
Copyright terms: Public domain | W3C validator |