I'm not sure I understand your question. Is your first statement, P implied Q, and P implies something unknown as well? Is your second statement, P implies Q, and not P implies something unknown? And then the third statement is simply Q?

Well, it seems to me at first look that crossing out - if that's what you're doing - is more work that just reading and understanding the logic - because in order to cross out correctly you already have to have understood the logic.

The point is that the crossing out is other logic than "classic" modus ponens, but it is a formal way that leds to a valid conclusion (necessarily true if premises are true). But is seems not to be a logical consequence of premises.

The question, then, is do you have an explicit "crossing out" rule that is not just a sleight-of-hand modus ponens? For example, (p=>q) = ~(p^~q). Can you do that with crossing out?

Obviously, the "crossing out" rule only works for certain premises and notations. My claim is that there are other "rules" with the same consequence for all logical system, which use always a linguistic notation (they are formal languages). For example, for (p=>q) = ~(p^~q) someone could interpret than "=>" means that we must cross out two "~" signs and one "^" sign, so pq=pq.
The point is that all notation system do not prevent the existence of heuristic rules that led both to formal and necessary conclusions. I try to show cases of logical luck.

Tautologies are logical truths.
In virtue of truth tables (p & q) -> q is a tautology.
and
((p -> q) & p) <-> (p & q), is a tautology.
therefore
((p -> q) & p) -> q is a tautology.