Metamath Proof Explorer


Theorem mulcan2ad

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

Ref Expression
Hypotheses mulcanad.1 ( 𝜑𝐴 ∈ ℂ )
mulcanad.2 ( 𝜑𝐵 ∈ ℂ )
mulcanad.3 ( 𝜑𝐶 ∈ ℂ )
mulcanad.4 ( 𝜑𝐶 ≠ 0 )
mulcan2ad.5 ( 𝜑 → ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) )
Assertion mulcan2ad ( 𝜑𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 mulcanad.1 ( 𝜑𝐴 ∈ ℂ )
2 mulcanad.2 ( 𝜑𝐵 ∈ ℂ )
3 mulcanad.3 ( 𝜑𝐶 ∈ ℂ )
4 mulcanad.4 ( 𝜑𝐶 ≠ 0 )
5 mulcan2ad.5 ( 𝜑 → ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) )
6 1 2 3 4 mulcan2d ( 𝜑 → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ↔ 𝐴 = 𝐵 ) )
7 5 6 mpbid ( 𝜑𝐴 = 𝐵 )