Defining implication relation for classical logic

It is a theorem or valid rule of replacement in classical logic that P implies Q is logically equivalent to not-P or Q, which means they can be replaced (in proofs) or defined (in axioms) by each other. It is well known that the equivalence is problematic as it is not actually valid. Specifically, from P implies Q, not-P or Q can be inferred (``Implication-to-disjunction'' is indeed valid), while from not-P or Q, P implies Q cannot be inferred (``Disjunction-to-implication'' is not valid), so the equivalence between them is invalid. This work aims to remove exactly the incorrect Disjunction-to-implication from classical logic (CL). The paper proposes a logical system (IRL), which has the properties (1) adding Disjunction-to-implication to IRL is simply CL, and (2) Disjunction-to-implication is independent of IRL, i.e. either Disjunction-to-implication or its negation cannot be derived in IRL. In other words, IRL is just the subsystem of CL with Disjunction-to-implication being exactly removed.