Metamath Proof Explorer


Theorem addcan2ad

Description: Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses muld.1 φA
addcomd.2 φB
addcand.3 φC
addcan2ad.4 φA+C=B+C
Assertion addcan2ad φA=B

Proof

Step Hyp Ref Expression
1 muld.1 φA
2 addcomd.2 φB
3 addcand.3 φC
4 addcan2ad.4 φA+C=B+C
5 1 2 3 addcan2d φA+C=B+CA=B
6 4 5 mpbid φA=B