Def P & Q == PQ

is mentioned by

Thm* (P1  P2)  (Q1  Q2)  P1 & Q1  P2 & Q2	[and_functionality_wrt_implies]
Thm* (P1  P2)  (Q1  Q2)  (P1 & Q1  P2 & Q2)	[and_functionality_wrt_iff]
Thm* B:(TProp). (x:T. A & B(x))  A & (x:T. B(x))	[exists_over_and_r]
Thm* A & True  A	[and_true_r]
Thm* True & A  A	[and_true_l]
Thm* A & False  False	[and_false_r]
Thm* False & A  False	[and_false_l]
Thm* Dec(A)  ((A & B)  A  B)	[not_over_and]
Thm* A  B  (A & B)	[not_over_and_b]
Thm* (A  B)  A & B	[not_over_or_a]
Thm* (A  B)  A & B	[not_over_or]
Thm* A & B  B & A	[and_comm]
Thm* A & (B & C)  (A & B) & C	[and_assoc]
Thm* SqStable(P)  SqStable(Q)  SqStable(P & Q)	[sq_stable__and]
Thm* Dec(P)  Dec(Q)  Dec(P & Q)	[decidable__and]
Def a = !x:T. Q(x) == Q(a) & (a':T. Q(a')  a' = a)	[uni_sat]
Def {!x:T | P(x)} == {x:T| P(x) & (y:T. P(y)  y = x) }	[unique_set]
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