![]() |
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 3009 | . 2 ⊢ (𝜑 → 𝐶 ≠ 𝐵) |
4 | 3netr4d.3 | . 2 ⊢ (𝜑 → 𝐷 = 𝐵) | |
5 | 3, 4 | neeqtrrd 3016 | 1 ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ≠ wne 2941 |
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 2942 |
This theorem is referenced by: infpssrlem4 10297 modsumfzodifsn 13905 mgm2nsgrplem4 18798 pmtr3ncomlem1 19334 isdrng2 20317 prmirredlem 21026 uvcf1 21331 dfac14lem 23103 i1fmullem 25193 fta1glem1 25665 fta1blem 25668 plydivlem4 25791 fta1lem 25802 cubic 26334 asinlem 26353 dchrn0 26733 lgsne0 26818 noextenddif 27151 noresle 27180 perpneq 27945 axlowdimlem14 28193 preimane 31873 cycpmco2lem6 32268 cycpmrn 32280 cntnevol 33164 subfacp1lem5 34113 fvtransport 34942 poimirlem1 36427 poimirlem6 36432 poimirlem7 36433 dalem4 38474 cdleme35sn2aw 39267 cdleme39n 39275 cdleme41fva11 39286 trlcone 39537 hdmaprnlem3N 40659 sticksstones2 40901 uvcn0 41062 flt0 41323 stoweidlem23 44674 2zrngnmlid 46749 2zrngnmrid 46750 zlmodzxznm 47080 line2y 47343 |
Copyright terms: Public domain | W3C validator |