# Metamath Proof Explorer

## Theorem divcan3

Description: A cancellation law for division. (Contributed by NM, 3-Feb-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion divcan3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{{B}{A}}{{B}}={A}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}{B}{A}={B}{A}$
2 simp2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {B}\in ℂ$
3 simp1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {A}\in ℂ$
4 2 3 mulcld ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {B}{A}\in ℂ$
5 3simpc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
6 divmul ${⊢}\left({B}{A}\in ℂ\wedge {A}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \left(\frac{{B}{A}}{{B}}={A}↔{B}{A}={B}{A}\right)$
7 4 3 5 6 syl3anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \left(\frac{{B}{A}}{{B}}={A}↔{B}{A}={B}{A}\right)$
8 1 7 mpbiri ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{{B}{A}}{{B}}={A}$