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)\leftrightarrow \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)\leftrightarrow 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)\leftrightarrow 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)\leftrightarrow \left(A\parallel \left(C-E\right)\vee A\parallel \left(C-\left(-E\right)\right)\right)\right)$$