# Metamath Proof Explorer

## Theorem acongeq12d

Description: Substitution deduction for alternating congruence. (Contributed by Stefan O'Rear, 3-Oct-2014)

Ref Expression
Hypotheses acongeq12d.1 ${⊢}{\phi }\to {B}={C}$
acongeq12d.2 ${⊢}{\phi }\to {D}={E}$
Assertion acongeq12d ${⊢}{\phi }\to \left(\left({A}\parallel \left({B}-{D}\right)\vee {A}\parallel \left({B}-\left(-{D}\right)\right)\right)↔\left({A}\parallel \left({C}-{E}\right)\vee {A}\parallel \left({C}-\left(-{E}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 acongeq12d.1 ${⊢}{\phi }\to {B}={C}$
2 acongeq12d.2 ${⊢}{\phi }\to {D}={E}$
3 1 2 oveq12d ${⊢}{\phi }\to {B}-{D}={C}-{E}$
4 3 breq2d ${⊢}{\phi }\to \left({A}\parallel \left({B}-{D}\right)↔{A}\parallel \left({C}-{E}\right)\right)$
5 2 negeqd ${⊢}{\phi }\to -{D}=-{E}$
6 1 5 oveq12d ${⊢}{\phi }\to {B}-\left(-{D}\right)={C}-\left(-{E}\right)$
7 6 breq2d ${⊢}{\phi }\to \left({A}\parallel \left({B}-\left(-{D}\right)\right)↔{A}\parallel \left({C}-\left(-{E}\right)\right)\right)$
8 4 7 orbi12d ${⊢}{\phi }\to \left(\left({A}\parallel \left({B}-{D}\right)\vee {A}\parallel \left({B}-\left(-{D}\right)\right)\right)↔\left({A}\parallel \left({C}-{E}\right)\vee {A}\parallel \left({C}-\left(-{E}\right)\right)\right)\right)$