X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flogic.ma;h=8f981d46924556ee885407a1320d147ef07aaad0;hb=ef3bdc4be26f6518a82a79c64e986253f7aeaa3c;hp=c80fa31f55c5469a97212e3c49431360e3e805fa;hpb=94188b0cbaff6340464d90cc13ee246ea7ec3284;p=helm.git

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index c80fa31f5..8f981d469 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -153,7 +153,28 @@ inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
 definition iff :=
  λ A,B. (A → B) ∧ (B → A).
 
-interpretation "iff" 'iff a b = (iff a b).  
+interpretation "iff" 'iff a b = (iff a b).
+
+lemma iff_sym: ∀A,B. A ↔ B → B ↔ A.
+#A #B * /3/ qed.
+
+lemma iff_trans:∀A,B,C. A ↔ B → B ↔ C → A ↔ C.
+#A #B #C * #H1 #H2 * #H3 #H4 % /3/ qed.
+
+lemma iff_not: ∀A,B. A ↔ B → ¬A ↔ ¬B.
+#A #B * #H1 #H2 % /3/ qed.
+
+lemma iff_and_l: ∀A,B,C. A ↔ B → C ∧ A ↔ C ∧ B.
+#A #B #C * #H1 #H2 % * /3/ qed.  
+
+lemma iff_and_r: ∀A,B,C. A ↔ B → A ∧ C ↔ B ∧ C.
+#A #B #C * #H1 #H2 % * /3/ qed.  
+
+lemma iff_or_l: ∀A,B,C. A ↔ B → C ∨ A ↔ C ∨ B.
+#A #B #C * #H1 #H2 % * /3/ qed.  
+
+lemma iff_or_r: ∀A,B,C. A ↔ B → A ∨ C ↔ B ∨ C.
+#A #B #C * #H1 #H2 % * /3/ qed.  
 
 (* cose per destruct: da rivedere *)