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 2827 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
4 | 1, 3 | neeqtrd 3085 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ≠ wne 3016 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-ne 3017 |
This theorem is referenced by: 3netr4d 3093 ttukeylem7 9926 modsumfzodifsn 13302 expnprm 16228 symgextf1lem 18479 isabvd 19522 flimclslem 22522 chordthmlem 25337 atandmtan 25425 dchrptlem3 25770 opphllem6 26466 unidifsnne 30224 pmtrcnel 30661 pmtrcnel2 30662 cycpmrn 30713 fedgmul 30927 signstfveq0a 31746 subfacp1lem5 32329 noetalem3 33117 ovoliunnfl 34816 voliunnfl 34818 volsupnfl 34819 cdleme40n 37486 cdleme40w 37488 cdlemg33c 37726 cdlemg33e 37728 trlcocnvat 37742 cdlemh2 37834 cdlemh 37835 cdlemj3 37841 cdlemk24-3 37921 cdlemkfid1N 37939 erng1r 38013 dvalveclem 38043 tendoinvcl 38122 tendolinv 38123 tendorinv 38124 dihatlat 38352 mapdpglem18 38707 mapdpglem22 38711 baerlem5amN 38734 baerlem5bmN 38735 baerlem5abmN 38736 mapdindp1 38738 mapdindp4 38741 hdmap14lem4a 38889 imo72b2lem0 40396 imo72b2lem2 40398 imo72b2lem1 40402 imo72b2 40406 islindeps2 44436 |
Copyright terms: Public domain | W3C validator |