Theorem acongeq12d

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

	Ref	Expression
Hypotheses	acongeq12d.1	|- ( ph -> B = C )
	acongeq12d.2	|- ( ph -> D = E )
Assertion	acongeq12d	|- ( ph -> ( ( A || ( B - D ) \/ A || ( B - -u D ) ) <-> ( A || ( C - E ) \/ A || ( C - -u E ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		acongeq12d.1	|- ( ph -> B = C )
2		acongeq12d.2	|- ( ph -> D = E )
3	1 2	oveq12d	|- ( ph -> ( B - D ) = ( C - E ) )
4	3	breq2d	|- ( ph -> ( A || ( B - D ) <-> A || ( C - E ) ) )
5	2	negeqd	|- ( ph -> -u D = -u E )
6	1 5	oveq12d	|- ( ph -> ( B - -u D ) = ( C - -u E ) )
7	6	breq2d	|- ( ph -> ( A || ( B - -u D ) <-> A || ( C - -u E ) ) )
8	4 7	orbi12d	|- ( ph -> ( ( A || ( B - D ) \/ A || ( B - -u D ) ) <-> ( A || ( C - E ) \/ A || ( C - -u E ) ) ) )