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")
    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
    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 T1,T2,T3,T4,T5 theorem