![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neeqtrrd | Structured version Visualization version GIF version |
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
Ref | Expression |
---|---|
neeqtrrd.1 | ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
neeqtrrd.2 | ⊢ (𝜑 → 𝐶 = 𝐵) |
Ref | Expression |
---|---|
neeqtrrd | ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeqtrrd.1 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵) | |
2 | neeqtrrd.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐵) | |
3 | 2 | eqcomd 2657 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
4 | 1, 3 | neeqtrd 2892 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 ≠ wne 2823 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 df-cleq 2644 df-ne 2824 |
This theorem is referenced by: 3netr4d 2900 ttukeylem7 9375 modsumfzodifsn 12783 znnenlem 14984 expnprm 15653 symgextf1lem 17886 isabvd 18868 flimclslem 21835 chordthmlem 24604 atandmtan 24692 dchrptlem3 25036 opphllem6 25689 signstfveq0a 30781 subfacp1lem5 31292 noetalem3 31990 ovoliunnfl 33581 voliunnfl 33583 volsupnfl 33584 cdleme40n 36073 cdleme40w 36075 cdlemg33c 36313 cdlemg33e 36315 trlcocnvat 36329 cdlemh2 36421 cdlemh 36422 cdlemj3 36428 cdlemk24-3 36508 cdlemkfid1N 36526 erng1r 36600 dvalveclem 36631 tendoinvcl 36710 tendolinv 36711 tendorinv 36712 dihatlat 36940 mapdpglem18 37295 mapdpglem22 37299 baerlem5amN 37322 baerlem5bmN 37323 baerlem5abmN 37324 mapdindp1 37326 mapdindp4 37329 hdmap14lem4a 37480 imo72b2lem0 38782 imo72b2lem2 38784 imo72b2lem1 38788 imo72b2 38792 islindeps2 42597 |
Copyright terms: Public domain | W3C validator |