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 2830 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | neeqtri 3088 | 1 ⊢ 𝐴 ≠ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ≠ wne 3016 |
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 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-ne 3017 |
This theorem is referenced by: 1one2o 8259 cflim2 9674 pnfnemnf 10685 resslem 16547 basendxnplusgndx 16598 plusgndxnmulrndx 16607 basendxnmulrndx 16608 slotsbhcdif 16683 rmodislmod 19633 cnfldfun 20487 xrsnsgrp 20511 zlmlem 20594 matvsca 20955 tnglem 23178 setsvtx 26748 resvlem 30832 limsucncmpi 33691 sn-1ne2 39038 |
Copyright terms: Public domain | W3C validator |