subneintr2d - Intuitionistic Logic Explorer

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

Theorem subneintr2d 8211

Description: Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcan2d 8207. (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 8210	. . 3 ⊢ (𝜑 → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵))
6	5	necon3bid 2365	. 2 ⊢ (𝜑 → ((𝐴 − 𝐶) ≠ (𝐵 − 𝐶) ↔ 𝐴 ≠ 𝐵))
7	1, 6	mpbird 166	1 ⊢ (𝜑 → (𝐴 − 𝐶) ≠ (𝐵 − 𝐶))

Colors of variables: wff set class

Syntax hints: → wi 4 ∈ wcel 2125 ≠ wne 2324 (class class class)co 5814 ℂcc 7709 − cmin 8025

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-14 2128 ax-ext 2136 ax-sep 4078 ax-pow 4130 ax-pr 4164 ax-setind 4490 ax-resscn 7803 ax-1cn 7804 ax-icn 7806 ax-addcl 7807 ax-addrcl 7808 ax-mulcl 7809 ax-addcom 7811 ax-addass 7813 ax-distr 7815 ax-i2m1 7816 ax-0id 7819 ax-rnegex 7820 ax-cnre 7822

This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1740 df-eu 2006 df-mo 2007 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ne 2325 df-ral 2437 df-rex 2438 df-reu 2439 df-rab 2441 df-v 2711 df-sbc 2934 df-dif 3100 df-un 3102 df-in 3104 df-ss 3111 df-pw 3541 df-sn 3562 df-pr 3563 df-op 3565 df-uni 3769 df-br 3962 df-opab 4022 df-id 4248 df-xp 4585 df-rel 4586 df-cnv 4587 df-co 4588 df-dm 4589 df-iota 5128 df-fun 5165 df-fv 5171 df-riota 5770 df-ov 5817 df-oprab 5818 df-mpo 5819 df-sub 8027

This theorem is referenced by: (None)

W3C validator