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 3080 | . 2 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
4 | 1, 3 | mpbir 232 | 1 ⊢ 𝐴 ≠ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ≠ wne 3016 |
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 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-ne 3017 |
This theorem is referenced by: eqnetrri 3087 notzfaus 5254 notzfausOLD 5255 2on0 8104 1n0 8110 noinfep 9112 card1 9386 fin23lem31 9754 s1nz 13951 bpoly4 15403 tan0 15494 resslem 16547 basendxnplusgndx 16598 plusgndxnmulrndx 16607 basendxnmulrndx 16608 slotsbhcdif 16683 rmodislmod 19633 cnfldfun 20487 xrsnsgrp 20511 matvsca 20955 ustuqtop1 22779 iaa 24843 tan4thpi 25029 ang180lem2 25315 mcubic 25352 quart1lem 25360 ex-lcm 28165 9p10ne21 28177 resvlem 30832 esumnul 31207 ballotth 31695 quad3 32811 bj-1upln0 34219 bj-2upln0 34233 bj-2upln1upl 34234 nn0rppwr 39062 sn-0ne2 39116 mncn0 39619 aaitgo 39642 stirlinglem11 42250 sec0 44757 2p2ne5 44797 |
Copyright terms: Public domain | W3C validator |