Formal Proof defined

Introduction to Mathematical logic Sixth edition Elliott Mendelson
1.4 An Axiom System for the Propositional Calculus page 28
A wf C is said to be a consequence in S of a set Γ of wfs if and only if there is a sequence B1, …, Bk of wfs such that C is Bk and, for each i, either Bi is an axiom or Bi is in Γ, or Bi is a direct consequence by some rule of inference of some of the preceding wfs in the sequence. Such a sequence is called a proof (or deduction) of C from Γ. The members of Γ are called the hypotheses or premisses of the proof. We use Γ ⊢ C as an abbreviation for “C is a consequence of Γ”…

If Γ is the empty set ∅, then ∅ ⊢ C if and only if C is a theorem. It is customary to omit the sign “∅” and simply write ⊢ C. Thus, ⊢ C is another way of asserting that C is a theorem.