diff --git a/axiomes de quantificateurs.md b/axiomes de quantificateurs.md
new file mode 100644
index 00000000..7657b15a
--- /dev/null
+++ b/axiomes de quantificateurs.md	
@@ -0,0 +1,12 @@
+---
+up:
+  - "[[règles de démonstration]]"
+tags:
+  - s/maths/logique
+aliases:
+---
+
+> [!definition] Définition
+> 1. $T \vdash \left[ \exists x f \leftrightarrow \neg \forall x \neg f \right]$
+> 2. $T \vdash [\forall x (f \rightarrow g) \to$
+^definition
\ No newline at end of file
diff --git a/règles de démonstration . tautologies.md b/règles de démonstration . tautologies.md
index b5e2d71f..11848d8b 100644
--- a/règles de démonstration . tautologies.md	
+++ b/règles de démonstration . tautologies.md	
@@ -8,4 +8,6 @@ aliases:
 
 > [!definition] Définition
 > Si $T \vdash f_1, \dots, T \vdash f_{n}$
+> et si $\varphi(x_1, \dots, x_{n})$ est une [[tautologie]] du calcul propositionnel
+> alors $T \vdash \varphi(f_1, \dots, f_{n})$
 ^definition
\ No newline at end of file
diff --git a/règles de démonstration . égalité.md b/règles de démonstration . égalité.md
new file mode 100644
index 00000000..41c277a6
--- /dev/null
+++ b/règles de démonstration . égalité.md	
@@ -0,0 +1,14 @@
+---
+up:
+  - "[[règles de démonstration]]"
+tags:
+  - s/maths/logique
+aliases:
+---
+
+> [!definition] Définition
+>  - $T \vdash x =x$
+>  - $T \vdash (x = y) \to (y = x)$
+>  - $T \vdash (x = y) \wedge (y = z) \to (x = z)$
+>  - $T \vdash (x_1 = y_1 \wedge \dots \wedge x_{n} = y_{n}) \to f$
+^definition
\ No newline at end of file