![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neeqtrd | Structured version Visualization version GIF version |
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
Ref | Expression |
---|---|
neeqtrd.1 | ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
neeqtrd.2 | ⊢ (𝜑 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
neeqtrd | ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeqtrd.1 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵) | |
2 | neeqtrd.2 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐶) | |
3 | 2 | neeq2d 3003 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶)) |
4 | 1, 3 | mpbid 222 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1631 ≠ wne 2943 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 df-cleq 2764 df-ne 2944 |
This theorem is referenced by: neeqtrrd 3017 3netr3d 3019 xaddass2 12285 xov1plusxeqvd 12525 issubdrg 19015 ply1scln0 19876 qsssubdrg 20020 alexsublem 22068 cphsubrglem 23196 cphreccllem 23197 mdegldg 24046 tglinethru 25752 footex 25834 poimirlem26 33768 lkrpssN 34972 lnatexN 35588 lhpexle2lem 35818 lhpexle3lem 35820 cdlemg47 36546 cdlemk54 36768 tendoinvcl 36914 lcdlkreqN 37432 mapdh8ab 37587 jm2.26lem3 38094 stoweidlem36 40767 |
Copyright terms: Public domain | W3C validator |