| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eqnetri | Structured version Visualization version GIF version | ||
| Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.) |
| Ref | Expression |
|---|---|
| eqnetr.1 | ⊢ 𝐴 = 𝐵 |
| eqnetr.2 | ⊢ 𝐵 ≠ 𝐶 |
| Ref | Expression |
|---|---|
| eqnetri | ⊢ 𝐴 ≠ 𝐶 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqnetr.2 | . 2 ⊢ 𝐵 ≠ 𝐶 | |
| 2 | eqnetr.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
| 3 | 2 | neeq1i 3005 | . 2 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
| 4 | 1, 3 | mpbir 231 | 1 ⊢ 𝐴 ≠ 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: = 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: eqnetrri 3012 notzfaus 5363 2on0 8522 1n0 8526 snnen2o 9273 noinfep 9700 card1 10008 fin23lem31 10383 s1nz 14645 bpoly4 16095 tan0 16187 nn0rppwr 16598 resslemOLD 17288 basendxnmulrndx 17339 basendxnmulrndxOLD 17340 plusgndxnmulrndx 17341 slotsbhcdif 17459 slotsbhcdifOLD 17460 symgvalstructOLD 19415 cnfldfunALTOLDOLD 21393 xrsnsgrp 21420 pzriprnglem4 21495 matvscaOLD 22422 ustuqtop1 24250 iaa 26367 tan4thpi 26556 tan4thpiOLD 26557 ang180lem2 26853 mcubic 26890 quart1lem 26898 nogt01o 27741 slotsinbpsd 28449 slotslnbpsd 28450 ex-lcm 30477 9p10ne21 30489 resvlemOLD 33358 esumnul 34049 ballotth 34540 quad3 35675 bj-1upln0 37010 bj-2upln0 37024 bj-2upln1upl 37025 tan3rdpi 42386 sn-0ne2 42436 flt0 42647 flt4lem5e 42666 mncn0 43151 aaitgo 43174 mnringnmulrdOLD 44229 stirlinglem11 46099 sec0 49279 2p2ne5 49317 |
| Copyright terms: Public domain | W3C validator |