--- /dev/null
+#u abandali
+#a h02
+
+#q q04d
+
+p <=> q, p & q <=> (p | q)
+
+#check TP
+
+p <=> q <-> p & q <=> (p | q)
+
+ 1) p & q <=> (p | q)
+ 2) (p & q => p | q) & (p | q => p & q) by equiv
+ 3) (!(p & q) | p | q) & (!(p | q) | p & q) by impl * 2
+ 4) (!p | !q | p | q) & (!(p | q) | p & q) by dm
+ 5) (true | !q | q) & (!(p | q) | p & q) by lem
+ 6) true & (!(p | q) | p & q) by simp1
+ 7) !(p | q) | p & q by simp1
+ 8) !p & !q | p & q by dm
+ 9) (!p & !q | p) & (!p & !q | q) by distr
+10) (!p | p) & (!q | p) & (!p | q) & (!q | q) by distr * 2
+11) true & (!q | p) & (!p | q) & true by lem * 2
+12) (!q | p) & (!p | q) by simp1 * 2
+13) (q => p) & (p => q) by impl * 2
+14) p <=> q by equiv