Rule 16: Theorem (Thm <number of theorem>) If T is a theorem, containing sentence letters such as "P," "Q," "R" and so on, an "instance" of that theorem may be written in as a new line in which every "P" has been replaced by exactly the same sentence, every "Q" has been replaced by exactly the same sentence (which can be different from the sentence written in for every "P"), and so on. 
Rs  (  Ba  Rs  ) 
Rs  (  Ba  Rs  ) 
Rs  (  Ba  Rs  ) 
(Mu v No)  (  (Hi ^ Gu)  (Mu v No)  ) 
(Iu Ge)  (  (Mu v No)  (Iu Ge)  ) 
Ba  (  {(Ja v Te) ^ (Wf [Ul Tm])}  Ba  ) 
{(Ja v Te) ^ (Wf [Ul Tm])}  (  [HeNi]  {(Ja v Te) ^ (Wf [Ul Tm])}  ) 
1.  (Hi Gu)(Hi ^ Gu) 
Instance  Not Instance 
2.  (Hi Gu)(Hi Gu) 
Instance  Not Instance 
3.  (Mu ^ No)(Mu v No) 
Instance  Not Instance 
4.  [Rs(BaRs)][Rs(BaRs)] 
Instance  Not Instance 
5.  {(Mu v No)[(Hi ^ Gu) (Mu v No)]}{(Mu v No)[(Hi ^ Gu) (Mu v No)]} 
Instance  Not Instance 
6.  BaRs 
Instance  Not Instance 
Theorems 3 & 4 (Exportation Laws) 3. [(P ^ Q) R] [P (QR)] 4. [(P ^ Q) R] [Q (PR)] 
1.  2.  3.  4.  5. 
6.  7.  8.  9.  10. 
11.  12.  13.  14.  15. 
16.  17.  18.  19.  20. 
