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

Metamath Proof Explorer

Theorem s3cl

Description: A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s3cl 
|- ( ( A e. X /\ B e. X /\ C e. X ) -> <" A B C "> e. Word X )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> A e. X )
2 simp2 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> B e. X )
3 simp3 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> C e. X )
4 1 2 3 s3cld 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> <" A B C "> e. Word X )