Metamath Proof Explorer


Theorem subneintr2d

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

Ref Expression
Hypotheses negidd.1 φA
pncand.2 φB
subaddd.3 φC
subneintr2d.4 φAB
Assertion subneintr2d φACBC

Proof

Step Hyp Ref Expression
1 negidd.1 φA
2 pncand.2 φB
3 subaddd.3 φC
4 subneintr2d.4 φAB
5 1 2 3 subcan2ad φAC=BCA=B
6 5 necon3bid φACBCAB
7 4 6 mpbird φACBC