Def P  Q == Q  P

is mentioned by

Thm* (P  Q)  P  Q	[not_functionality_wrt_implies]
Thm* (P1  P2)  (Q1  Q2)  (P1  Q1)  P2  Q2	[implies_functionality_wrt_implies]
Def P  Q == (P  Q) & (P  Q)	[iff]

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