Def P  Q == (P  Q) & (P  Q)

is mentioned by

Thm* (P  Q)  (Q  P)  (P  Q)	[implies_antisymmetry]
Thm* (P  Q)  (P  Q)	[squash_functionality_wrt_iff]
Thm* (P1  P2)  (Q1  Q2)  (P1  Q1  P2  Q2)	[or_functionality_wrt_iff]
Thm* (P  Q)  (P  Q)	[not_functionality_wrt_iff]
Thm* P,Q:(SProp). Thm* S = T  (x:S. P(x)  Q(x))  ((x:S. P(x))  (y:T. Q(y)))	[exists_functionality_wrt_iff]
Thm* P,Q:(SProp). Thm* S = T  (x:S. P(x)  Q(x))  ((x:S. P(x))  (y:T. Q(y)))	[all_functionality_wrt_iff]
Thm* (P1  P2)  (Q1  Q2)  ((P1  Q1)  (P2  Q2))	[iff_functionality_wrt_iff]
Thm* (P  Q)  (Dec(P)  Dec(Q))	[decidable_functionality]
Thm* (P1  P2)  (Q1  Q2)  ((P1  Q1)  (P2  Q2))	[implies_functionality_wrt_iff]
Thm* (P1  P2)  (Q1  Q2)  (P1 & Q1  P2 & Q2)	[and_functionality_wrt_iff]
Thm* (P  Q)  (Q  R)  (P  R)	[iff_transitivity]
Thm* Q:(TProp). (x:T. Q(x))  (x:T. Q(x))	[not_over_exists]
Thm* B:(TProp). (x:T. A & B(x))  A & (x:T. B(x))	[exists_over_and_r]
Thm* A  True  True	[or_true_r]
Thm* True  A  True	[or_true_l]
Thm* A  False  A	[or_false_r]
Thm* False  A  A	[or_false_l]
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_or_a]
Thm* (A  B)  A & B	[not_over_or]
Thm* A  B  B  A	[or_comm]
Thm* A  (B  C)  (A  B)  C	[or_assoc]
Thm* A & B  B & A	[and_comm]
Thm* A & (B & C)  (A & B) & C	[and_assoc]
Thm* (A  B)  (B  A)	[iff_symmetry]
Thm* Dec(A)  (A  A)	[dneg_elim_a]
Thm* SqStable(P)  (P  P)	[squash_elim]
Thm* SqStable(P)  SqStable(Q)  SqStable(P  Q)	[sq_stable__iff]
Thm* Dec(A)  (A  B)  Dec(B)	[iff_preserves_decidability]
Thm* Dec(P)  Dec(Q)  Dec(P  Q)	[decidable__iff]

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