Metamath Proof Explorer

Theorem subcan2ad

Description: Cancellation law for subtraction. Deduction form of subcan2 . Generalization of subcan2d . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses negidd.1 φ A
pncand.2 φ B
subaddd.3 φ C
Assertion subcan2ad φ A C = B C A = B


Step Hyp Ref Expression
1 negidd.1 φ A
2 pncand.2 φ B
3 subaddd.3 φ C
4 subcan2 A B C A C = B C A = B
5 1 2 3 4 syl3anc φ A C = B C A = B