é uma subfórmula de
uma fórmula 
se é uma
sequência de símbolos consecutivos de que é uma
fórmula.
As subfórmulas de são as fórmulas que
ocorrem na árvore de .
Regra das Fórmulas Tautologicamente Equivalentes (TE): Se
, 
, 
,
são fórmulas do cálculo proposicional tais que
é subfórmula de , e se
se obtem de substituindo
alguma ocorrência de por , com 
, então 
.
Algumas Tautologias Úteis nas Simplificações. Usamos o
símbolo 
para designar uma tautologia
qualquer e 
para uma contradição
genérica.
