![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqnetri | Structured version Visualization version Unicode 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 2688 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbir 214 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-ext 2432 |
This theorem depends on definitions: df-bi 190 df-cleq 2445 df-ne 2624 |
This theorem is referenced by: eqnetrri 2695 notzfaus 4551 2on0 7178 1n0 7184 noinfep 8152 card1 8389 fin23lem31 8760 bpoly4 14123 tan0 14216 resslem 15193 slotsbhcdif 15329 xrsnsgrp 19015 matbas 19449 matplusg 19450 matvsca 19452 ustuqtop1 21267 iaa 23293 tan4thpi 23481 ang180lem2 23751 mcubic 23785 quart1lem 23793 resvlem 28601 esumnul 28876 ballotth 29376 ballotthOLD 29414 quad3 30308 bj-1upln0 31605 bj-2upln0 31619 bj-2upln1upl 31620 mncn0 36000 aaitgo 36030 stirlinglem11 38003 plusgndxnmulrndx 40278 basendxnmulrndx 40279 sec0 40805 2p2ne5 40862 |
Copyright terms: Public domain | W3C validator |