Nuprl - Proof: d-sub transitivity 1

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

1. D1 : Dsys
2. D2 : Dsys
3. D3 : Dsys
4.

i:Id. M(i)

M(i)
5.

i:Id. M(i)

M(i)
6. i : Id

M(i)

By:	Using [`M2',M(i)] (BackThru Thm* M1,M2,M3:MsgA. M1 M2 M2 M3 M1 M3) THEN BackThruSomeHyp

Generated subgoals:

None

About:

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