La eliminación del bicondicional es el nombre de dos reglas de inferencia válidas de la lógica proposicional. Esto nos permite inferir un condicional de un bicondicional. Si ${\displaystyle (P\leftrightarrow Q)}$ es verdadero, entonces ${\displaystyle (P\to Q)}$ es verdadero y ${\displaystyle (Q\to P)}$ también lo será.^[1]​ Por ejemplo, si bien es cierto que estoy respirando si y sólo si estoy vivo, entonces es verdad que si estoy respirando, estoy vivo; Asimismo, es verdad que si estoy vivo, estoy respirando. Las reglas pueden ser establecidas formalmente como sigue:

${\displaystyle {\begin{array}{cl}&P\leftrightarrow Q\\\hline \therefore &P\to Q\\\end{array))}$

y

${\displaystyle {\begin{array}{cl}&P\leftrightarrow Q\\\hline \therefore &Q\to P\\\end{array))}$

donde la regla es que cada vez que una instancia "${\displaystyle (P\leftrightarrow Q)}$" aparezca en una línea de prueba, tanto "${\displaystyle (P\to Q)}$" como "${\displaystyle (Q\to P)}$" puede colocarse en la línea siguiente;

La regla de eliminación del bicondicional puede escribirse en notación subsiguiente:

${\displaystyle (P\leftrightarrow Q)\vdash (P\to Q)}$

y

${\displaystyle (P\leftrightarrow Q)\vdash (Q\to P)}$

donde ${\displaystyle \vdash }$ es el símbolo metalógico lo que significa que ${\displaystyle (P\to Q)}$ en el primer caso, y ${\displaystyle (Q\to P)}$ en otros son consecuencia sintáctica de ${\displaystyle (P\leftrightarrow Q)}$ en algún sistema lógico;

o como una declaración de verdadera tautología funcional o teorema de la lógica proposicional:

${\displaystyle (P\leftrightarrow Q)\to (P\to Q)}$ ${\displaystyle (P\leftrightarrow Q)\to (Q\to P)}$

donde ${\displaystyle P}$ y ${\displaystyle Q}$ son proposiciones expresadas en algún sistema formal.

• Esta obra contiene una traducción total derivada de «Biconditional elimination» de Wikipedia en inglés, concretamente de esta versión, publicada por sus editores bajo la Licencia de documentación libre de GNU y la Licencia Creative Commons Atribución-CompartirIgual 4.0 Internacional.