Are there rules of Logic dealing with the implies operator? I'm just beginning a course in discrete mathematics and I'm learning a few of the basic laws to prove propositions. I understand how to use propositions that use the logical connectives, AND , OR, NOT. However I'm not sure how to prove a proposition that has an implies operator. For example prove the following is a tautology.
$(p\land (p\implies q))\implies q$ 

There are two possible answers. One, your language doesn't really contain the $\implies$ operator, and it is thought of as a shorthand (as in user3123's answer): $$a \implies b \text{ is a shorthand for } \lnot a \lor b.$$
Two, your language does include it, and then you have some axioms expressing its "meaning". For example, you could have a system with only $\lnot$ and $\implies$, having the following axioms
$$ A \implies (B \implies A) $$
$$ (A \implies B) \implies ((B \implies C) \implies (A \implies C)) $$
$$ (A \implies B) \implies (\lnot B \implies \lnot A) $$
and Modus Ponens as the only inference rule: given $A$ and $A \implies B$, deduce $B$. This system is complete (can prove every true proposition). The other connectives are then shorthands:
$$ A \lor B \text{ stands for } \lnot A \implies B $$
$$ A \land B \text{ stands for } \lnot(\lnot A \lor \lnot B) $$
