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")
    T5("T5 Hyp. syllogism")
    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)")
    T13("T13 Excluded middle")
    T14("T14 Non-contradiction")
    T15("T15 Explosion")
    T16("T16 Commutation (or)")
    T17("T17 Commutation (and)")
    T18("T18 Distribution")
    T19("T19 Deduction thm")
    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
    A2 --> T5
    T1 --> T5
    MP --> T5
    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
    DefOr --> T13
    T2 --> T13
    T3 --> T13
    MP --> T13
    DefAnd --> T14
    T4 --> T14
    MP --> T14
    DefAnd --> T15
    A1 --> T15
    A2 --> T15
    MP --> T15
    DefOr --> T16
    T4 --> T16
    MP --> T16
    DefAnd --> T17
    T9 --> T17
    MP --> T17
    DefAnd --> T18
    DefOr --> T18
    T6 --> T18
    T7 --> T18
    T8 --> T18
    T9 --> T18
    MP --> T18
    A1 --> T19
    A2 --> T19
    MP --> T19
    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,T5,T6,T7,T8,T9,T10,T11,T12,T13,T14,T15,T16,T17,T18,T19 theorem