Difference?: Semantic consequence vs. Implication

I am currently studying Dirk Van Dalen's Logic and Structure, in which I encountered two very similar concepts:

Semantic consequence:$$φ \vDash θ$$ and $$θ \vDash σ$$ $$\Rightarrow φ \vDash σ$$

A tautology using the implication connective:$$\vDash ((φ \rightarrow θ) \land (θ \rightarrow σ)) \rightarrow (φ \rightarrow σ)$$

I have come to understand that $$\Rightarrow$$ is taken to be a meta-logical symbol,one that the reader uses to reason; And that $$\rightarrow$$ is taken to be one of the connectives in the set PROP, with which one has constructed the formal language.

My question is: In the everyday reasoning of a mathematician trying to prove something, is he using semantic consequece?

Or is it something only utilized by the logician, trying to construct tautologies for the mathematician to use?

• Usual math reasoning is to prove theorems form axioms and already proven theorems. Thus in a math proof we have that the theorems are consequence of the axioms. – Mauro ALLEGRANZA Feb 8 at 8:09
• Regarding $⇒ φ ⊨ σ$ (that is badly written; it must be e.g. "$φ \vdash σ ⇒ φ ⊨ σ$") van Dalen uses it (and in this way he generates some conclusion) as "if..., then..." in the meta-language. – Mauro ALLEGRANZA Feb 8 at 8:09
• See also the post Meaning of symbols $\vdash$ and $\models$ – Mauro ALLEGRANZA Feb 8 at 8:14