graph TD
    A1("A1 Weakening")
    A2("A2 Distrib. of impl.")
    A3("A3 Contraposition")
    MP("MP MP")
    T1("T1 Self-implication")
    T2("T2 Double neg. elim")
    T3("T3 Double neg. intro")
    T4("T4 Transposition")
    DefOr("DefOr Def. disjunction")
    DefAnd("DefAnd Def. conjunction")
    DefIff("DefIff Def. biconditional")
    T6("T6 Addition (orI)")
    T7("T7 Simplification (andE)")
    T8("T8 Simplification (andE)")
    T9("T9 Conjunction (andI)")
    T10("T10 Material impl.")
    T11("T11 De Morgan (1)")
    T12("T12 De Morgan (2)")
    A1 --> T1
    A2 --> T1
    MP --> T1
    A3 --> T2
    T1 --> T2
    MP --> T2
    A1 --> T3
    A3 --> T3
    MP --> T3
    A3 --> T4
    T2 --> T4
    T3 --> T4
    MP --> T4
    A1 --> DefOr
    A2 --> DefOr
    A3 --> DefOr
    MP --> DefOr
    DefOr --> DefAnd
    A3 --> DefAnd
    MP --> DefAnd
    DefAnd --> DefIff
    T9 --> DefIff
    MP --> DefIff
    DefOr --> T6
    A1 --> T6
    MP --> T6
    DefAnd --> T7
    A1 --> T7
    A3 --> T7
    MP --> T7
    DefAnd --> T8
    A1 --> T8
    A3 --> T8
    MP --> T8
    A1 --> T9
    A2 --> T9
    MP --> T9
    DefOr --> T10
    T4 --> T10
    MP --> T10
    DefAnd --> T11
    DefOr --> T11
    T4 --> T11
    T6 --> T11
    MP --> T11
    DefAnd --> T12
    DefOr --> T12
    T4 --> T12
    MP --> T12
    classDef axiom fill:#e74c3c,color:#fff,stroke:#c0392b
    classDef definition fill:#3498db,color:#fff,stroke:#2980b9
    classDef theorem fill:#1abc9c,color:#fff,stroke:#16a085
    class A1,A2,A3,MP axiom
    class DefOr,DefAnd,DefIff definition
    class T1,T2,T3,T4,T6,T7,T8,T9,T10,T11,T12 theorem