Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ltrnco Structured version   Unicode version

Theorem ltrnco 31453
 Description: The composition of two translations is a translation. Part of proof of Lemma G of [Crawley] p. 116, line 15 on p. 117. (Contributed by NM, 31-May-2013.)
Hypotheses
Ref Expression
ltrnco.h
ltrnco.t
Assertion
Ref Expression
ltrnco

Proof of Theorem ltrnco
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 957 . . 3
2 ltrnco.h . . . . 5
3 eqid 2435 . . . . 5
4 ltrnco.t . . . . 5
52, 3, 4ltrnldil 30856 . . . 4
72, 3, 4ltrnldil 30856 . . . 4
92, 3ldilco 30850 . . 3
101, 6, 8, 9syl3anc 1184 . 2
11 simp11 987 . . . . 5
12 simp2l 983 . . . . . 6
13 simp3l 985 . . . . . 6
1412, 13jca 519 . . . . 5
15 simp2r 984 . . . . . 6
16 simp3r 986 . . . . . 6
1715, 16jca 519 . . . . 5
18 simp12 988 . . . . 5
19 simp13 989 . . . . 5
20 eqid 2435 . . . . . 6
21 eqid 2435 . . . . . 6
22 eqid 2435 . . . . . 6
23 eqid 2435 . . . . . 6
2420, 21, 22, 23, 2, 4cdlemg41 31452 . . . . 5
2511, 14, 17, 18, 19, 24syl122anc 1193 . . . 4
26253exp 1152 . . 3
2726ralrimivv 2789 . 2
2820, 21, 22, 23, 2, 3, 4isltrn 30853 . . 3