Metamath Proof Explorer

Theorem nnacan

Description: Cancellation law for addition of natural numbers. (Contributed by NM, 27-Oct-1995) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnacan ⊢A∈ω∧B∈ω∧C∈ω→A+𝑜B=A+𝑜C↔B=C

Proof

Step Hyp Ref Expression
1 nnaword ⊢B∈ω∧C∈ω∧A∈ω→B⊆C↔A+𝑜B⊆A+𝑜C
2 1 3comr ⊢A∈ω∧B∈ω∧C∈ω→B⊆C↔A+𝑜B⊆A+𝑜C
3 nnaword ⊢C∈ω∧B∈ω∧A∈ω→C⊆B↔A+𝑜C⊆A+𝑜B
4 3 3com13 ⊢A∈ω∧B∈ω∧C∈ω→C⊆B↔A+𝑜C⊆A+𝑜B
5 2 4 anbi12d ⊢A∈ω∧B∈ω∧C∈ω→B⊆C∧C⊆B↔A+𝑜B⊆A+𝑜C∧A+𝑜C⊆A+𝑜B
6 5 bicomd ⊢A∈ω∧B∈ω∧C∈ω→A+𝑜B⊆A+𝑜C∧A+𝑜C⊆A+𝑜B↔B⊆C∧C⊆B
7 eqss ⊢A+𝑜B=A+𝑜C↔A+𝑜B⊆A+𝑜C∧A+𝑜C⊆A+𝑜B
8 eqss ⊢B=C↔B⊆C∧C⊆B
9 6 7 8 3bitr4g ⊢A∈ω∧B∈ω∧C∈ω→A+𝑜B=A+𝑜C↔B=C