(5steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eqmod fun 1 1

1. m : 
2. a : 
3. a' : 
4. b : 
5. b' : 
6. b = b' mod m
7. a = b mod m
8. a' = a mod m
  a' = b' mod m


By: (FwdThru Thm* m,a,b,c:. (a = b mod m (b = c mod m (a = c mod m) [8;7])
THEN
(FwdThru Thm* m,a,b,c:. (a = b mod m (b = c mod m (a = c mod m) [6;9])


Generated subgoals:

None

About:
intimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(5steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc