![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > negeq | Unicode version |
Description: Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.) |
Ref | Expression |
---|---|
negeq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 5882 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-neg 8129 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | df-neg 8129 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3eqtr4g 2235 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-rex 2461 df-v 2739 df-un 3133 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3810 df-br 4004 df-iota 5178 df-fv 5224 df-ov 5877 df-neg 8129 |
This theorem is referenced by: negeqi 8149 negeqd 8150 neg11 8206 negf1o 8337 recexre 8533 negiso 8910 elz 9253 znegcl 9282 zaddcllemneg 9290 elz2 9322 zindd 9369 infrenegsupex 9592 supinfneg 9593 infsupneg 9594 supminfex 9595 ublbneg 9611 eqreznegel 9612 negm 9613 qnegcl 9634 xnegeq 9825 ceilqval 10303 exp3val 10519 expnegap0 10525 m1expcl2 10539 negfi 11231 dvdsnegb 11810 infssuzex 11944 infssuzcldc 11946 zsupssdc 11949 lcmneg 12068 pcexp 12303 pcneg 12318 znnen 12393 mulgneg2 12970 negcncf 13981 negfcncf 13982 lgsdir2lem4 14325 ex-ceil 14360 |
Copyright terms: Public domain | W3C validator |