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

Theorem ltrnco 30908
 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 955 . . 3
2 ltrnco.h . . . . 5
3 eqid 2283 . . . . 5
4 ltrnco.t . . . . 5
52, 3, 4ltrnldil 30311 . . . 4
72, 3, 4ltrnldil 30311 . . . 4
92, 3ldilco 30305 . . 3
101, 6, 8, 9syl3anc 1182 . 2
11 simp11 985 . . . . 5
12 simp2l 981 . . . . . 6
13 simp3l 983 . . . . . 6
1412, 13jca 518 . . . . 5
15 simp2r 982 . . . . . 6
16 simp3r 984 . . . . . 6
1715, 16jca 518 . . . . 5
18 simp12 986 . . . . 5
19 simp13 987 . . . . 5
20 eqid 2283 . . . . . 6
21 eqid 2283 . . . . . 6
22 eqid 2283 . . . . . 6
23 eqid 2283 . . . . . 6
2420, 21, 22, 23, 2, 4cdlemg41 30907 . . . . 5
2511, 14, 17, 18, 19, 24syl122anc 1191 . . . 4
26253exp 1150 . . 3
2726ralrimivv 2634 . 2
2820, 21, 22, 23, 2, 3, 4isltrn 30308 . . 3