subneintr2d - Intuitionistic Logic Explorer

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

Theorem subneintr2d 8673

Description: Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcan2d 8669. (Contributed by David Moews, 28-Feb-2017.)

**Hypotheses**
Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
pncand.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
subaddd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)
subneintr2d.4	⊢ (𝜑 → 𝐴 ≠ 𝐵)

**Assertion**
Ref	Expression
subneintr2d	⊢ (𝜑 → (𝐴 − 𝐶) ≠ (𝐵 − 𝐶))

**Proof of Theorem subneintr2d**
Step	Hyp	Ref	Expression
1		subneintr2d.4	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		negidd.1	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		pncand.2	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℂ)
4		subaddd.3	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℂ)
5	2, 3, 4	subcan2ad 8672	. . 3 ⊢ (𝜑 → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵))
6	5	necon3bid 2461	. 2 ⊢ (𝜑 → ((𝐴 − 𝐶) ≠ (𝐵 − 𝐶) ↔ 𝐴 ≠ 𝐵))
7	1, 6	mpbird 167	1 ⊢ (𝜑 → (𝐴 − 𝐶) ≠ (𝐵 − 𝐶))

Colors of variables: wff set class

Syntax hints: → wi 4 ∈ wcel 2209 ≠ wne 2420 (class class class)co 6075 ℂcc 8167 − cmin 8487

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 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-sep 4244 ax-pow 4306 ax-pr 4341 ax-setind 4679 ax-resscn 8261 ax-1cn 8262 ax-icn 8264 ax-addcl 8265 ax-addrcl 8266 ax-mulcl 8267 ax-addcom 8269 ax-addass 8271 ax-distr 8273 ax-i2m1 8274 ax-0id 8277 ax-rnegex 8278 ax-cnre 8280

This theorem depends on definitions: df-bi 117 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-ral 2533 df-rex 2534 df-reu 2535 df-rab 2537 df-v 2823 df-sbc 3052 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-pw 3687 df-sn 3711 df-pr 3712 df-op 3714 df-uni 3931 df-br 4126 df-opab 4188 df-id 4433 df-xp 4775 df-rel 4776 df-cnv 4777 df-co 4778 df-dm 4779 df-iota 5332 df-fun 5374 df-fv 5380 df-riota 6028 df-ov 6078 df-oprab 6079 df-mpo 6080 df-sub 8489

This theorem is referenced by: (None)

W3C validator