![]() |
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 2887 | . 2 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
4 | 1, 3 | mpbir 221 | 1 ⊢ 𝐴 ≠ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = 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: eqnetrri 2894 notzfaus 4870 2on0 7614 1n0 7620 noinfep 8595 card1 8832 fin23lem31 9203 s1nz 13423 bpoly4 14834 tan0 14925 resslem 15980 basendxnplusgndx 16036 plusgndxnmulrndx 16045 basendxnmulrndx 16046 slotsbhcdif 16127 rmodislmod 18979 cnfldfun 19806 xrsnsgrp 19830 matbas 20267 matplusg 20268 matvsca 20270 ustuqtop1 22092 iaa 24125 tan4thpi 24311 ang180lem2 24585 mcubic 24619 quart1lem 24627 ex-lcm 27445 resvlem 29959 esumnul 30238 ballotth 30727 quad3 31690 bj-1upln0 33122 bj-2upln0 33136 bj-2upln1upl 33137 mncn0 38026 aaitgo 38049 stirlinglem11 40619 sec0 42829 2p2ne5 42872 |
Copyright terms: Public domain | W3C validator |