Nuprl - Proof: eqmod transitivity 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eqmod transitivity 1

1. m :

2. a :

3. b :

4. c :

5. m | a-b
6. m | b-c

m | a-c

By:	(FwdThru Thm* a,b1,b2:. a \| b1 a \| b2 a \| b1+b2 [5;6]) THEN (OnMClauses [0;-1] ArithSimp)

Generated subgoals:

None

About:

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