Q == (P 
Q) & (P Q)
Thm* 
A,B:Prop. (A B) 
Prop
A == A False
Thm* A:Prop. (A) Prop
Q == Q P
Thm* A,B:Prop. (A B) Prop
| iff |
Def P Q == (P Q) & (P Q)
Thm* |
| not |
Def A == A False
Thm* |
| rev_implies |
Def P Q == Q P
Thm* |
About:
 |  |  |  |  |  |  |