Formal logic is the science of deductively valid inferences or logical truths. It studies how conclusions follow from premises due to the structure of arguments alone, independent of their topic and content.
Hilbertstyle systems and Gentzenstyle systems.
Gentzen’s Natural Deduction is a pretty neat one.
 <PREMISE 1>
 <PREMISE 2>
 ...
 <PREMISE N>
 <rulename>
 <CONCLUSION>
 A
 B
 conjintro
 A ∧ B
 A ∧ B
 conjeliml
 A
 A ∧ B
 conjelimr
 B
 A
 disjintrol
 A ∨ B
 B
 disjintror
 A ∨ B
 A ∨ B

  A
 
  C

  B
 
  C
 disjelim
 C
 A

 B
 implintro
A ==> B
 A ==> B
 A
 implelim
 B
  A
 
  ⊥

 negintro
 ¬A
 A
 ¬A
 negelim
 ⊥
 ⊥
 contraelim
 A
  ¬A
 
  ⊥
 proofbycontra
 A
  x
 
  P[x]
 forallintro
 ∀ α P[x/α]
As a sidecondition—the x
must not “escape” its scope.
Demonstrate.
 ∀ α P[α]
 forallelim
 P[α/x]
 P[t]
 existsintro
 ∃ α P[t/α]
As a side note—not all occurrences of term t
have to be replaced with α
s.
Demonstrate.
 ∃ α P[α]

  P[α/x]
 
  F

 existselim
 F
As a sidecondition—the x
must not “escape” its scope.
Do these resemble something you know? Maybe focus on the implication introduction and elimination, forall introduction …
Theorem proving is not magic!
Let’s do some light theorem proving.