Theorem seqeq123d

Description: Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013)

	Ref	Expression
Hypotheses	seqeq123d.1	⊢ ( 𝜑 → 𝑀 = 𝑁 )
	seqeq123d.2	⊢ ( 𝜑 → + = 𝑄 )
	seqeq123d.3	⊢ ( 𝜑 → 𝐹 = 𝐺 )
Assertion	seqeq123d	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) = seq 𝑁 ( 𝑄 , 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		seqeq123d.1	⊢ ( 𝜑 → 𝑀 = 𝑁 )
2		seqeq123d.2	⊢ ( 𝜑 → + = 𝑄 )
3		seqeq123d.3	⊢ ( 𝜑 → 𝐹 = 𝐺 )
4	1	seqeq1d	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) = seq 𝑁 ( + , 𝐹 ) )
5	2	seqeq2d	⊢ ( 𝜑 → seq 𝑁 ( + , 𝐹 ) = seq 𝑁 ( 𝑄 , 𝐹 ) )
6	3	seqeq3d	⊢ ( 𝜑 → seq 𝑁 ( 𝑄 , 𝐹 ) = seq 𝑁 ( 𝑄 , 𝐺 ) )
7	4 5 6	3eqtrd	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) = seq 𝑁 ( 𝑄 , 𝐺 ) )