![]() |
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 3000 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶)) |
4 | 1, 3 | mpbid 231 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ≠ wne 2939 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2723 df-ne 2940 |
This theorem is referenced by: neeqtrrd 3014 3netr3d 3016 xaddass2 13179 xov1plusxeqvd 13425 smndex2dnrinv 18739 ablsimpgfindlem1 19900 issubdrg 20296 qsssubdrg 20893 ply1scln0 21699 alexsublem 23432 cphsubrglem 24578 cphreccllem 24579 mdegldg 25468 nosep2o 27067 noetainflem4 27125 tglinethru 27641 footexALT 27723 footexlem2 27725 sdrgdvcl 32145 sdrginvcl 32146 0ringprmidl 32298 0ringmon1p 32340 irngnzply1lem 32451 poimirlem26 36177 lkrpssN 37698 lnatexN 38315 lhpexle2lem 38545 lhpexle3lem 38547 cdlemg47 39272 cdlemk54 39494 tendoinvcl 39640 lcdlkreqN 40158 mapdh8ab 40313 jm2.26lem3 41383 stoweidlem36 44397 |
Copyright terms: Public domain | W3C validator |