Add some convenience ND-rules

source/math.mmt

@@ -86,6 +86,15 @@ theory NaturalDeduction : ur:?LF =
 	 not_elim : {A} ⊦ ¬ ¬ A ⟶ ⊦ A ❙
 
 	 tnd : {A} ⊦ A ∨ ¬A ❘ // = [A: bool] not_introduction ([p : ⊦ (¬A ∧ ¬¬A)] fals_introduction (not_elim (and_elim_right p)) (and_elim_left p)) ❙
+
+	/T Some more rules for convenience. ❙
+
+        or_introduction_right :  {A,B} ⊦ A ⟶ ⊦ (A ∨ B) ❘ # orinr 3❙
+        or_introduction_left :  {A,B} ⊦ B ⟶ ⊦ (A ∨ B) ❘ # orinl 3❙
+        implication_introduction : {A,B} (⊦ A ⟶ ⊦ B) ⟶ ⊦ A ⇒ B ❘ # impli 3❙
+        equiv_introduction : {A,B} ⊦ (A ⇒ B) ⟶ ⊦ (B ⇒ A) ⟶ ⊦ (A ⇔ B) ❘ # equivi 3 4❙
+        or_elimination : {A,B} ⊦ (A ∨ B) ⟶ (⊦ A ⟶ ⊦ C) ⟶ (⊦ B ⟶ ⊦ C) ⟶ ⊦ C ❘ # orelim 3 4 5❙
+        modus_ponens : {A,B} (⊦ A ⇒ B) ⟶ ⊦ A ⟶ ⊦ B ❘ # MP 3 4 ❙
 	 
 	 /T basic axioms governing Equality. Again, all the type parameters can be left implicit ❙
 	 eq_refl : {t:𝒰 100,A: t} ⊦ A ≐ A ❘ # eq_refl 2❙