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 2827 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | neeqtri 3085 | 1 ⊢ 𝐴 ≠ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = 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: 1one2o 8258 cflim2 9673 pnfnemnf 10684 resslem 16545 basendxnplusgndx 16596 plusgndxnmulrndx 16605 basendxnmulrndx 16606 slotsbhcdif 16681 rmodislmod 19631 cnfldfun 20485 xrsnsgrp 20509 zlmlem 20592 matvsca 20953 tnglem 23176 setsvtx 26747 resvlem 30831 limsucncmpi 33690 sn-1ne2 39036 |
Copyright terms: Public domain | W3C validator |