Metamath Proof Explorer


Theorem mulcanad

Description: Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcand . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses mulcanad.1 φ A
mulcanad.2 φ B
mulcanad.3 φ C
mulcanad.4 φ C 0
mulcanad.5 φ C A = C B
Assertion mulcanad φ A = B

Proof

Step Hyp Ref Expression
1 mulcanad.1 φ A
2 mulcanad.2 φ B
3 mulcanad.3 φ C
4 mulcanad.4 φ C 0
5 mulcanad.5 φ C A = C B
6 1 2 3 4 mulcand φ C A = C B A = B
7 5 6 mpbid φ A = B