Description: Equality theorem for a length 4 word. (Contributed by Mario Carneiro, 27-Feb-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | s2eqd.1 | ⊢ ( 𝜑 → 𝐴 = 𝑁 ) | |
s2eqd.2 | ⊢ ( 𝜑 → 𝐵 = 𝑂 ) | ||
s3eqd.3 | ⊢ ( 𝜑 → 𝐶 = 𝑃 ) | ||
s4eqd.4 | ⊢ ( 𝜑 → 𝐷 = 𝑄 ) | ||
Assertion | s4eqd | ⊢ ( 𝜑 → 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 = 〈“ 𝑁 𝑂 𝑃 𝑄 ”〉 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s2eqd.1 | ⊢ ( 𝜑 → 𝐴 = 𝑁 ) | |
2 | s2eqd.2 | ⊢ ( 𝜑 → 𝐵 = 𝑂 ) | |
3 | s3eqd.3 | ⊢ ( 𝜑 → 𝐶 = 𝑃 ) | |
4 | s4eqd.4 | ⊢ ( 𝜑 → 𝐷 = 𝑄 ) | |
5 | 1 2 3 | s3eqd | ⊢ ( 𝜑 → 〈“ 𝐴 𝐵 𝐶 ”〉 = 〈“ 𝑁 𝑂 𝑃 ”〉 ) |
6 | 4 | s1eqd | ⊢ ( 𝜑 → 〈“ 𝐷 ”〉 = 〈“ 𝑄 ”〉 ) |
7 | 5 6 | oveq12d | ⊢ ( 𝜑 → ( 〈“ 𝐴 𝐵 𝐶 ”〉 ++ 〈“ 𝐷 ”〉 ) = ( 〈“ 𝑁 𝑂 𝑃 ”〉 ++ 〈“ 𝑄 ”〉 ) ) |
8 | df-s4 | ⊢ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 = ( 〈“ 𝐴 𝐵 𝐶 ”〉 ++ 〈“ 𝐷 ”〉 ) | |
9 | df-s4 | ⊢ 〈“ 𝑁 𝑂 𝑃 𝑄 ”〉 = ( 〈“ 𝑁 𝑂 𝑃 ”〉 ++ 〈“ 𝑄 ”〉 ) | |
10 | 7 8 9 | 3eqtr4g | ⊢ ( 𝜑 → 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 = 〈“ 𝑁 𝑂 𝑃 𝑄 ”〉 ) |