![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neeqtrri | Structured version Visualization version GIF version |
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
Ref | Expression |
---|---|
neeqtrr.1 | ⊢ 𝐴 ≠ 𝐵 |
neeqtrr.2 | ⊢ 𝐶 = 𝐵 |
Ref | Expression |
---|---|
neeqtrri | ⊢ 𝐴 ≠ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeqtrr.1 | . 2 ⊢ 𝐴 ≠ 𝐵 | |
2 | neeqtrr.2 | . . 3 ⊢ 𝐶 = 𝐵 | |
3 | 2 | eqcomi 2660 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | neeqtri 2895 | 1 ⊢ 𝐴 ≠ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ≠ wne 2823 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 df-cleq 2644 df-ne 2824 |
This theorem is referenced by: cflim2 9123 pnfnemnf 10132 resslem 15980 basendxnplusgndx 16036 plusgndxnmulrndx 16045 basendxnmulrndx 16046 slotsbhcdif 16127 rmodislmod 18979 cnfldfun 19806 xrsnsgrp 19830 zlmlem 19913 matbas 20267 matplusg 20268 matvsca 20270 tnglem 22491 setsvtx 25972 resvlem 29959 limsucncmpi 32569 |
Copyright terms: Public domain | W3C validator |