What is the type of "A implies B"? There are many deductions with different flavor to show that is logical to think proposition $A \implies B$ is true when A is false. For example:
In classical logic, why is  (p⇒q) True if both  p  and  q  are False?
In classical logic, why is  (p⇒q) True if  p  is False and  q  is True?
All of above responses directly or indirectly, use this statement:

“p implies q” means that if p is true, then q must also be true.

My question is not in about "Why that may be formally logical". I want to know what is the type of above statement about the meaning of "$\implies$". Is that a definition? An axiom? A theorem? or ...? Really I want to find the root and reliable source reference which presented that meaning. I think there must be a famous book or reference in about logic which is the root of that meaning and all mathematicians accept that. So I can rely to that for similar questions.
Update:
In WIKIPEDIA, you can see:           

Definitions of the material conditional:
  Logicians have many
  different views on the nature of material implication and approaches
  to explain its sense ...
As a truth function
  In classical logic, the compound p→q is logically equivalent to the negative compound: not both p and not q.
As a formal connective
  ... Unlike the truth-functional one, this approach to logical connectives permits the examination of structurally identical propositional forms in various logical systems, where somewhat different properties may be demonstrated.         

If above vision be true, then “p implies q” means that ... will be a definition. Is this true?
 A: Short answer: It is a definition. Long answer:
The definition of the conditional in logic is simply a choice, in the same way that we choose that multiplication has higher precedence over addition in arithmetic. Sure, there are reasons for the choice, but it is silly to expect there to be some famous reference from which it comes, especially when the reasons for the choice are easily arrived at independently by every logician.
Specifically, in natural language we have conditional expressions of the form "If A then B.". Now this has many possible meanings and subtle nuances, such as when used with the subjunctive or imperative. It is completely reasonable to want to choose one specific meaning for the logical form "$A \to B$" just so that it is tidy. Since logic was meant to be for reasoning about facts, the obvious choice is the meaning when both A and B are declarative sentences. That meaning considers the natural language sentence to be valid exactly according to a certain truth table, and we simply adopt that same truth table for the logical form.
By doing so we of course end up with a logical connective that does not capture any other meaning of the natural language conditional except that which we chose.
A: My position, as already given in my answer to one of the linked questions would be that the statement

$p\Rightarrow q$ means that if $p$ is true, then $q$ is also true

is an explanation of how mathematicians use the English words "if" and "then", assuming that you already know the meaning of the $\Rightarrow$ symbol (which is defined by its truth table).
A: 'A implies B' is a statement that, in the metalanguage of a logical system, says that the conditional 'A ⟹ B' is tautological. Basically, it's a meta-statement about a relationship of two statements in the system.
