![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > negeqd | GIF 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 7826 | . 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → -𝐴 = -𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1299 -cneg 7805 |
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 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-3an 932 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-rex 2381 df-v 2643 df-un 3025 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-br 3876 df-iota 5024 df-fv 5067 df-ov 5709 df-neg 7807 |
This theorem is referenced by: negdi 7890 mulneg2 8025 mulm1 8029 eqord2 8113 mulreim 8232 apneg 8239 divnegap 8327 div2negap 8356 recgt0 8466 infrenegsupex 9239 supminfex 9242 ceilqval 9920 ceilid 9929 modqcyc2 9974 monoord2 10091 reneg 10481 imneg 10489 cjcj 10496 cjneg 10503 minmax 10840 minabs 10846 telfsumo2 11075 sinneg 11231 tannegap 11233 sincossq 11253 odd2np1 11365 oexpneg 11369 modgcd 11474 limcimolemlt 12513 ex-ceil 12541 |
Copyright terms: Public domain | W3C validator |