![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > negeqd | Unicode version |
Description: Equality deduction for negatives. (Contributed by NM, 14-May-1999.) |
Ref | Expression |
---|---|
negeqd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
negeqd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negeqd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | negeq 7772 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-rex 2376 df-v 2635 df-un 3017 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-br 3868 df-iota 5014 df-fv 5057 df-ov 5693 df-neg 7753 |
This theorem is referenced by: negdi 7836 mulneg2 7971 mulm1 7975 eqord2 8059 mulreim 8178 apneg 8185 divnegap 8270 div2negap 8299 recgt0 8408 infrenegsupex 9181 supminfex 9184 ceilqval 9862 ceilid 9871 modqcyc2 9916 monoord2 10027 reneg 10417 imneg 10425 cjcj 10432 cjneg 10439 minmax 10776 minabs 10782 telfsumo2 11010 sinneg 11166 tannegap 11168 sincossq 11188 odd2np1 11300 oexpneg 11304 modgcd 11409 ex-ceil 12370 |
Copyright terms: Public domain | W3C validator |