![]() |
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 3002 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶)) |
4 | 1, 3 | mpbid 231 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ≠ wne 2941 |
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 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2729 df-ne 2942 |
This theorem is referenced by: neeqtrrd 3016 3netr3d 3018 xaddass2 13123 xov1plusxeqvd 13369 smndex2dnrinv 18685 ablsimpgfindlem1 19845 issubdrg 20200 qsssubdrg 20809 ply1scln0 21614 alexsublem 23347 cphsubrglem 24493 cphreccllem 24494 mdegldg 25383 nosep2o 26982 noetainflem4 27040 tglinethru 27407 footexALT 27489 footexlem2 27491 sdrgdvcl 31902 sdrginvcl 31903 0ringprmidl 32044 0ringmon1p 32086 irngnzply1lem 32184 poimirlem26 36042 lkrpssN 37563 lnatexN 38180 lhpexle2lem 38410 lhpexle3lem 38412 cdlemg47 39137 cdlemk54 39359 tendoinvcl 39505 lcdlkreqN 40023 mapdh8ab 40178 jm2.26lem3 41234 stoweidlem36 44178 |
Copyright terms: Public domain | W3C validator |