| 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 1540 ≠ wne 2940 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ne 2941 |
| This theorem is referenced by: f1ounsn 7292 infpssrlem4 10346 modsumfzodifsn 13985 mgm2nsgrplem4 18934 pmtr3ncomlem1 19491 isdrng2 20743 prmirredlem 21483 uvcf1 21812 dfac14lem 23625 i1fmullem 25729 fta1glem1 26207 fta1blem 26210 plydivlem4 26338 fta1lem 26349 cubic 26892 asinlem 26911 dchrn0 27294 lgsne0 27379 noextenddif 27713 noresle 27742 perpneq 28722 axlowdimlem14 28970 preimane 32680 cycpmco2lem6 33151 cycpmrn 33163 irngnminplynz 33755 cntnevol 34229 subfacp1lem5 35189 fvtransport 36033 poimirlem1 37628 poimirlem6 37633 poimirlem7 37634 dalem4 39667 cdleme35sn2aw 40460 cdleme39n 40468 cdleme41fva11 40479 trlcone 40730 hdmaprnlem3N 41852 sticksstones2 42148 expeq1d 42359 uvcn0 42552 flt0 42647 stoweidlem23 46038 gpg3kgrtriex 48045 2zrngnmlid 48171 2zrngnmrid 48172 zlmodzxznm 48414 line2y 48676 |
| Copyright terms: Public domain | W3C validator |