 Let L be a language containing a unary connective ~ (negation) and a binary connective → (implication). A logical system in a language extending L is called a connexive logic if AT, AT′, BT, and BT′ are theorems and, moreover, implication is non-symmetric, i.e., (A → B) → (B → A) fails to be a theorem (so that → can hardly be understood as a bi-conditional). This is the now standard notion of connexive logic. The connective → in a system of connexive logic is said to be a connexive implication.