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 2846 | . 2 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
4 | 1, 3 | mpbir 220 | 1 ⊢ 𝐴 ≠ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ≠ wne 2780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-cleq 2603 df-ne 2782 |
This theorem is referenced by: eqnetrri 2853 notzfaus 4766 2on0 7456 1n0 7462 noinfep 8440 card1 8677 fin23lem31 9048 s1nz 13239 bpoly4 14629 tan0 14720 resslem 15760 slotsbhcdif 15903 xrsnsgrp 19601 matbas 20038 matplusg 20039 matvsca 20041 ustuqtop1 21855 iaa 23884 tan4thpi 24070 ang180lem2 24340 mcubic 24374 quart1lem 24382 ex-lcm 26707 resvlem 29162 esumnul 29437 ballotth 29926 quad3 30818 bj-1upln0 32190 bj-2upln0 32204 bj-2upln1upl 32205 mncn0 36728 aaitgo 36751 stirlinglem11 38977 plusgndxnmulrndx 41743 basendxnmulrndx 41744 sec0 42300 2p2ne5 42353 |
Copyright terms: Public domain | W3C validator |