Deducción natural/Reglas de eliminación

Conectiva	Nombre de la regla	Abreviación	Formalización	Cálculo de secuentes
$\neg \,$	Doble negación	$E\neg \,$	${\begin{matrix}{\underline {\quad p\quad }}\\{\overline {\;\neg \neg p\;}}\end{matrix}}$	$\neg \neg p\leftrightarrow p$
$\land \,$	Eliminación de la conjunción	$E\land \,$	${\begin{matrix}p\land q\\\hline p\end{matrix}}\qquad {\begin{matrix}p\land q\\\hline q\end{matrix}}$	$p\land q\to p$ $p\land q\to q$
$\lor \,$	Eliminación de la disyunción	$E\lor \,$	${\begin{matrix}p\lor q\\p\to r\\q\to r\\\hline r\end{matrix}}\qquad {\begin{matrix}\neg p\lor \neg q\\r\to p\\r\to q\\\hline \neg r\end{matrix}}$	$(p\lor q)\land (p\to r)\land (q\to r)\to r$ $(\neg p\lor \neg q)\land (r\to p)\land (r\to q)\to \neg r$
$\to \,$	Modus ponendo ponens	$MP$	${\begin{matrix}p\to q\\p\\\hline q\end{matrix}}$	$(p\to q)\land p\to q$
	Modus tollendo tollens	$MT$	${\begin{matrix}p\to q\\\neg q\\\hline \neg p\end{matrix}}$	$(p\to q)\land \neg q\to \neg p$
$\leftrightarrow \,$	Eliminación del bicondicional	$E\leftrightarrow \,$	${\begin{matrix}p\leftrightarrow q\\\hline p\to q\end{matrix}}\qquad {\begin{matrix}p\leftrightarrow q\\\hline q\to p\end{matrix}}$	$p\leftrightarrow q\to p\to q$ $p\leftrightarrow q\to q\to p$