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 3080 | . 2 ⊢ (𝜑 → 𝐶 ≠ 𝐵) |
4 | 3netr4d.3 | . 2 ⊢ (𝜑 → 𝐷 = 𝐵) | |
5 | 3, 4 | neeqtrrd 3087 | 1 ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ≠ wne 3013 |
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 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-ne 3014 |
This theorem is referenced by: infpssrlem4 9716 modsumfzodifsn 13300 mgm2nsgrplem4 18024 pmtr3ncomlem1 18530 isdrng2 19441 prmirredlem 20568 uvcf1 20864 dfac14lem 22153 i1fmullem 24222 fta1glem1 24686 fta1blem 24689 plydivlem4 24812 fta1lem 24823 cubic 25354 asinlem 25373 dchrn0 25753 lgsne0 25838 perpneq 26427 axlowdimlem14 26668 preimane 30343 cycpmco2lem6 30700 cycpmrn 30712 cntnevol 31386 subfacp1lem5 32328 noextenddif 33072 noresle 33097 fvtransport 33390 poimirlem1 34774 poimirlem6 34779 poimirlem7 34780 dalem4 36681 cdleme35sn2aw 37474 cdleme39n 37482 cdleme41fva11 37493 trlcone 37744 hdmaprnlem3N 38866 uvcn0 39029 stoweidlem23 42185 2zrngnmlid 44148 2zrngnmrid 44149 zlmodzxznm 44480 line2y 44670 |
Copyright terms: Public domain | W3C validator |