![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > neeq2d | Structured version Unicode version |
Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
Ref | Expression |
---|---|
neeq1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
neeq2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeq1d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eqeq2d 2468 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | necon3bid 2710 |
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 1592 ax-4 1603 ax-ext 2432 |
This theorem depends on definitions: df-bi 185 df-cleq 2446 df-ne 2650 |
This theorem is referenced by: neeq12dOLD 2732 neeq2 2735 neeqtrd 2747 fndifnfp 6019 infpssrlem4 8590 sqr2irr 13653 dsmmval 18294 dsmmbas2 18297 frlmbas 18315 frlmbasOLD 18316 dfcon2 19165 alexsublem 19758 uc1pval 21754 mon1pval 21756 dchrsum2 22750 usgrcyclnl1 23705 eigorth 25421 eighmorth 25547 wlimeq12 27923 nofulllem5 28014 limsucncmpi 28458 pridlval 29004 maxidlval 29010 stoweidlem43 30009 f12dfv 30317 f13dfv 30318 numclwwlkovq 30863 lshpset 32986 lduallkr3 33170 isatl 33307 cdlemk42 34948 |
Copyright terms: Public domain | W3C validator |