Theorem acongeq12d

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

	Ref	Expression
Hypotheses	acongeq12d.1	⊢ ( 𝜑 → 𝐵 = 𝐶 )
	acongeq12d.2	⊢ ( 𝜑 → 𝐷 = 𝐸 )
Assertion	acongeq12d	⊢ ( 𝜑 → ( ( 𝐴 ∥ ( 𝐵 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐷 ) ) ↔ ( 𝐴 ∥ ( 𝐶 − 𝐸 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐸 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		acongeq12d.1	⊢ ( 𝜑 → 𝐵 = 𝐶 )
2		acongeq12d.2	⊢ ( 𝜑 → 𝐷 = 𝐸 )
3	1 2	oveq12d	⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) = ( 𝐶 − 𝐸 ) )
4	3	breq2d	⊢ ( 𝜑 → ( 𝐴 ∥ ( 𝐵 − 𝐷 ) ↔ 𝐴 ∥ ( 𝐶 − 𝐸 ) ) )
5	2	negeqd	⊢ ( 𝜑 → - 𝐷 = - 𝐸 )
6	1 5	oveq12d	⊢ ( 𝜑 → ( 𝐵 − - 𝐷 ) = ( 𝐶 − - 𝐸 ) )
7	6	breq2d	⊢ ( 𝜑 → ( 𝐴 ∥ ( 𝐵 − - 𝐷 ) ↔ 𝐴 ∥ ( 𝐶 − - 𝐸 ) ) )
8	4 7	orbi12d	⊢ ( 𝜑 → ( ( 𝐴 ∥ ( 𝐵 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐷 ) ) ↔ ( 𝐴 ∥ ( 𝐶 − 𝐸 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐸 ) ) ) )