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 φ A B
Assertion subneintr2d φ A C B C


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