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 2824 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
4 | 1, 3 | neeqtrd 3082 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ≠ wne 3013 |
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 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-ne 3014 |
This theorem is referenced by: 3netr4d 3090 ttukeylem7 9925 modsumfzodifsn 13300 expnprm 16226 symgextf1lem 18477 isabvd 19520 flimclslem 22520 chordthmlem 25337 atandmtan 25425 dchrptlem3 25769 opphllem6 26465 unidifsnne 30223 pmtrcnel 30660 pmtrcnel2 30661 cycpmrn 30712 fedgmul 30926 signstfveq0a 31745 subfacp1lem5 32328 noetalem3 33116 ovoliunnfl 34815 voliunnfl 34817 volsupnfl 34818 cdleme40n 37484 cdleme40w 37486 cdlemg33c 37724 cdlemg33e 37726 trlcocnvat 37740 cdlemh2 37832 cdlemh 37833 cdlemj3 37839 cdlemk24-3 37919 cdlemkfid1N 37937 erng1r 38011 dvalveclem 38041 tendoinvcl 38120 tendolinv 38121 tendorinv 38122 dihatlat 38350 mapdpglem18 38705 mapdpglem22 38709 baerlem5amN 38732 baerlem5bmN 38733 baerlem5abmN 38734 mapdindp1 38736 mapdindp4 38739 hdmap14lem4a 38887 imo72b2lem0 40394 imo72b2lem2 40396 imo72b2 40403 islindeps2 44466 |
Copyright terms: Public domain | W3C validator |