This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem seqeq123d

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

Ref Expression
Hypotheses seqeq123d.1 ⊢ φ → M = N
seqeq123d.2 ⊢ φ → + ˙ = Q
seqeq123d.3 ⊢ φ → F = G
Assertion seqeq123d ⊢ φ → seq M + ˙ F = seq N Q G

Proof

Step Hyp Ref Expression
1 seqeq123d.1 ⊢ φ → M = N
2 seqeq123d.2 ⊢ φ → + ˙ = Q
3 seqeq123d.3 ⊢ φ → F = G
4 1 seqeq1d ⊢ φ → seq M + ˙ F = seq N + ˙ F
5 2 seqeq2d ⊢ φ → seq N + ˙ F = seq N Q F
6 3 seqeq3d ⊢ φ → seq N Q F = seq N Q G
7 4 5 6 3eqtrd ⊢ φ → seq M + ˙ F = seq N Q G