[math] (1) (\phi) \rightarrow ((\psi) \rightarrow (\phi))\\ (2) ((\phi) \rightarrow (\psi)) \rightarrow ((\phi) \rightarrow (\psi) \rightarrow (\pi)) \rightarrow ((\phi) \rightarrow (\pi))\\ (3) (\phi) \rightarrow (\psi) \rightarrow (\phi) \& (\psi)\\ (4) (\phi) \& (\psi) \rightarrow (\phi)\\ (5) (\phi) \& (\psi) \rightarrow (\psi)\\ (6) (\phi) \rightarrow (\phi) \vee (\psi)\\ (7) (\psi) \rightarrow (\phi) \vee (\psi)\\ (8) ((\phi) \rightarrow (\pi)) \rightarrow ((\psi) \rightarrow (\pi)) \rightarrow ((\phi) \vee (\psi) \rightarrow (\pi))\\ (9) ((\phi) \rightarrow (\psi)) \rightarrow ((\phi) \rightarrow \neg (\psi)) \rightarrow \neg (\phi)\\ (10) \neg \neg (\phi) \rightarrow (\phi)\\ [/math]
[math] (11) \forall{x}(\psi) \rightarrow (\psi[x := \alpha])\\ (12) (\psi[x := \alpha]) \rightarrow \exists{x}(\psi) \\ [/math]
[math] (A1) a = b \rightarrow a' = b' \\ (A2) a = b \rightarrow a = c \rightarrow b = c \\ (A3) a' = b' \rightarrow a = b \\ (A4) \neg a' = 0 \\ (A5) a + b' = (a+b)' \\ (A6) a + 0 = a \\ (A7) a \cdot 0 = a \\ (A8) a \cdot b' = a \cdot b + a \\ (A9) (\psi [x := 0]) \& \forall{x}((\psi) \rightarrow (\psi) [x := x']) \rightarrow (\psi)\\ [/math]
<tex> (E1) a = b \rightarrow (a = c \rightarrow b = c)\\ (E2) a = b \rightarrow (a \cdot c = b \cdot c)\\ (E3) a = b \rightarrow (c \cdot a = c \cdot b)\\ (G1) a \cdot (b \cdot c) = (a \cdot b) \cdot c\\ (G2) a \cdot 1 = a\\ (G3)a \cdot a ^ {-1} = 1\\
