Def pq == p  q

is mentioned by

Thm* p,q:. pq  (p  q)	[assert_of_bimplies]
Thm* u,v:. uv  u  v	[assert_functionality_wrt_bimplies]
Thm* u,v,w:. uv  vw  uw	[bimplies_transitivity]
Thm* u,v:. u = v  uv	[bimplies_weakening]
Def pq == qp	[rev_bimplies]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html