# Metamath Proof Explorer

## Theorem ablpnpcan

Description: Cancellation law for mixed addition and subtraction. ( pnpcan analog.) (Contributed by NM, 29-May-2015)

Ref Expression
Hypotheses ablsubadd.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
ablsubsub.g ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
ablsubsub.x ${⊢}{\phi }\to {X}\in {B}$
ablsubsub.y ${⊢}{\phi }\to {Y}\in {B}$
ablsubsub.z ${⊢}{\phi }\to {Z}\in {B}$
ablpnpcan.g ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
ablpnpcan.x ${⊢}{\phi }\to {X}\in {B}$
ablpnpcan.y ${⊢}{\phi }\to {Y}\in {B}$
ablpnpcan.z ${⊢}{\phi }\to {Z}\in {B}$
Assertion ablpnpcan

### Proof

Step Hyp Ref Expression
1 ablsubadd.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
4 ablsubsub.g ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
5 ablsubsub.x ${⊢}{\phi }\to {X}\in {B}$
6 ablsubsub.y ${⊢}{\phi }\to {Y}\in {B}$
7 ablsubsub.z ${⊢}{\phi }\to {Z}\in {B}$
8 ablpnpcan.g ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
9 ablpnpcan.x ${⊢}{\phi }\to {X}\in {B}$
10 ablpnpcan.y ${⊢}{\phi }\to {Y}\in {B}$
11 ablpnpcan.z ${⊢}{\phi }\to {Z}\in {B}$
12 1 2 3 ablsub4
13 4 5 6 5 7 12 syl122anc
14 ablgrp ${⊢}{G}\in \mathrm{Abel}\to {G}\in \mathrm{Grp}$
15 4 14 syl ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
16 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
17 1 16 3 grpsubid
18 15 5 17 syl2anc
19 18 oveq1d
20 1 3 grpsubcl
21 15 6 7 20 syl3anc
22 1 2 16 grplid
23 15 21 22 syl2anc
24 13 19 23 3eqtrd