mulneg12 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > mulneg12		Unicode version

Theorem mulneg12 8506

Description: Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.)

**Assertion**
Ref	Expression
mulneg12	$/\$

**Proof of Theorem mulneg12**
Step	Hyp	Ref	Expression
1		mulneg1 8504	. 2 $/\$
2		mulneg2 8505	. 2 $/\$
3	1, 2	eqtr4d 2243	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wceq 1373

wcel 2178 (class class class)co 5969

cc 7960

cmul 7967

cneg 8281

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-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-14 2181 ax-ext 2189 ax-sep 4179 ax-pow 4235 ax-pr 4270 ax-setind 4604 ax-resscn 8054 ax-1cn 8055 ax-icn 8057 ax-addcl 8058 ax-addrcl 8059 ax-mulcl 8060 ax-addcom 8062 ax-mulcom 8063 ax-addass 8064 ax-distr 8066 ax-i2m1 8067 ax-0id 8070 ax-rnegex 8071 ax-cnre 8073

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ne 2379 df-ral 2491 df-rex 2492 df-reu 2493 df-rab 2495 df-v 2779 df-sbc 3007 df-dif 3177 df-un 3179 df-in 3181 df-ss 3188 df-pw 3629 df-sn 3650 df-pr 3651 df-op 3653 df-uni 3866 df-br 4061 df-opab 4123 df-id 4359 df-xp 4700 df-rel 4701 df-cnv 4702 df-co 4703 df-dm 4704 df-iota 5252 df-fun 5293 df-fv 5299 df-riota 5924 df-ov 5972 df-oprab 5973 df-mpo 5974 df-sub 8282 df-neg 8283

This theorem is referenced by: mul2neg 8507 crim 11330 efi4p 12189 sinneg 12198 cosneg 12199 efmival 12205 negdvdsb 12279 divalglemex 12394 bezoutlemaz 12485 bezoutlembz 12486 dvrecap 15346