Metamath Proof Explorer


Theorem s4eqd

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 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ⟨“ 𝑁 𝑂 𝑃 𝑄 ”⟩ )

Proof

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 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ⟨“ 𝑁 𝑂 𝑃 𝑄 ”⟩ )