Theorem seqeq123d

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

	Ref	Expression
Hypotheses	seqeq123d.1	|- ( ph -> M = N )
	seqeq123d.2	|- ( ph -> .+ = Q )
	seqeq123d.3	|- ( ph -> F = G )
Assertion	seqeq123d	|- ( ph -> seq M ( .+ , F ) = seq N ( Q , G ) )

Proof

Step	Hyp	Ref	Expression
1		seqeq123d.1	|- ( ph -> M = N )
2		seqeq123d.2	|- ( ph -> .+ = Q )
3		seqeq123d.3	|- ( ph -> F = G )
4	1	seqeq1d	|- ( ph -> seq M ( .+ , F ) = seq N ( .+ , F ) )
5	2	seqeq2d	|- ( ph -> seq N ( .+ , F ) = seq N ( Q , F ) )
6	3	seqeq3d	|- ( ph -> seq N ( Q , F ) = seq N ( Q , G ) )
7	4 5 6	3eqtrd	|- ( ph -> seq M ( .+ , F ) = seq N ( Q , G ) )