Eliminação bicondicional
# Eliminação bicondicional

Eliminação bicondicional são duas regras de inferência validas da lógica proposicional. Ela permite inferir um condicional de um bicondicional. Se $(P\leftrightarrow Q)$ é verdadeiro, logo $(P\to Q)$ é verdadeiro, e $(Q\to P)$ também será. Por exemplo, se é verdade que eu estou respirando se e somente se estou vivo, então é verdade que se estou respirando, estou vivo; Igualmente, é verdade que se estou vivo, estou respirando. As regras podem ser estabelecidas formalmente como mostrado a seguir:
    ${\frac {(P\leftrightarrow Q)}{\therefore (P\to Q)}}$
e
    ${\frac {(P\leftrightarrow Q)}{\therefore (Q\to P)}}$
Onde a regra é que sempre que uma instância de "$(P\leftrightarrow Q)$" aparecer em uma linha da prova, ambos "$(P\to Q)$" ou "$(Q\to P)$" podem ser colocados na linha subsequente;

## Notação formal

A regra da eliminação bicondicional pode ser escrita na notação de sequentes:
    $(P\leftrightarrow Q)\vdash (P\to Q)$
e
    $(P\leftrightarrow Q)\vdash (Q\to P)$
onde $\vdash$ é o símbolo da metalógica que significa que $(P\to Q)$, no primeiro caso, e $(Q\to P)$ nos outros são consequência sintática de $(P\leftrightarrow Q)$ em algum sistema lógica;
ou como a afirmação da verdade funcional tautologia ou teorema da lógica proposicional:
    $(P\leftrightarrow Q)\to (P\to Q)$
    $(P\leftrightarrow Q)\to (Q\to P)$
onde $P$, e $Q$ são proposições expressas em algum sistema formal.