| 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 2746 | . 2 ⊢ 𝐵 = 𝐶 |
| 4 | 1, 3 | neeqtri 3013 | 1 ⊢ 𝐴 ≠ 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: = 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: nlim1 8527 nlim2 8528 1one2o 8684 cflim2 10303 pnfnemnf 11316 resslemOLD 17288 basendxnmulrndx 17339 basendxnmulrndxOLD 17340 plusgndxnmulrndx 17341 slotsbhcdif 17459 slotsbhcdifOLD 17460 symgvalstructOLD 19415 cnfldfunALTOLDOLD 21393 xrsnsgrp 21420 zlmlemOLD 21528 matvscaOLD 22422 tnglemOLD 24654 slotsinbpsd 28449 slotslnbpsd 28450 setsvtx 29052 resvlemOLD 33358 limsucncmpi 36446 sn-1ne2 42300 mnringbasedOLD 44231 mnringaddgdOLD 44237 mnringscadOLD 44242 mnringvscadOLD 44244 |
| Copyright terms: Public domain | W3C validator |