| 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 2743 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
| 4 | 1, 3 | neeqtrd 3010 | 1 ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ≠ wne 2940 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ne 2941 |
| This theorem is referenced by: 3netr4d 3018 ttukeylem7 10555 modsumfzodifsn 13985 expnprm 16940 symgextf1lem 19438 isabvd 20813 flimclslem 23992 chordthmlem 26875 atandmtan 26963 dchrptlem3 27310 noetasuplem4 27781 opphllem6 28760 nrt2irr 30492 unidifsnne 32554 pmtrcnel 33109 pmtrcnel2 33110 cycpmrn 33163 qsdrnglem2 33524 fedgmul 33682 irngnzply1 33741 irredminply 33757 signstfveq0a 34591 subfacp1lem5 35189 ovoliunnfl 37669 voliunnfl 37671 volsupnfl 37672 cdleme40n 40470 cdleme40w 40472 cdlemg33c 40710 cdlemg33e 40712 trlcocnvat 40726 cdlemh2 40818 cdlemh 40819 cdlemj3 40825 cdlemk24-3 40905 cdlemkfid1N 40923 erng1r 40997 dvalveclem 41027 tendoinvcl 41106 tendolinv 41107 tendorinv 41108 dihatlat 41336 mapdpglem18 41691 mapdpglem22 41695 baerlem5amN 41718 baerlem5bmN 41719 baerlem5abmN 41720 mapdindp1 41722 mapdindp4 41725 hdmap14lem4a 41873 uvcn0 42552 prjspner1 42636 nlimsuc 43454 imo72b2lem2 44180 imo72b2 44185 gpg5nbgrvtx03starlem2 48025 gpg5nbgrvtx13starlem2 48028 islindeps2 48400 fucofvalne 49020 |
| Copyright terms: Public domain | W3C validator |