H1 = A -> (B -> A) H2 = ((A -> B) -> A) -> A H3 = (A -> B) -> ((B -> C) -> (A -> C)) H4 = A & B -> A H5 = A & B -> B H6 = (A -> B) -> ((A -> C) -> (A -> B & C)) H7 = A -> A | B H8 = B -> A | B H9 = (A -> C) -> ((B -> C) -> (A | B -> C)) H10 = A <-> B -> (A -> B) H11 = A <-> B -> (B -> A) H12 = (A -> B) -> ((B -> A) -> A <-> B) H13 = (A -> B) -> (not B -> not A) H14 = A -> not (not A) H15 = not (not A) -> Amit Abtrennungs- (mopo) und Einsetzungsregel (sub) weitere Formeln erzeugen.
Beispiel: wir wollen x -> x ableiten.