# Metamath Proof Explorer

## Theorem nanbi

Description: Biconditional in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007) (Proof shortened by Wolf Lammen, 27-Jun-2020)

Ref Expression
Assertion nanbi ${⊢}\left({\phi }↔{\psi }\right)↔\left(\left({\phi }⊼{\psi }\right)⊼\left(\left({\phi }⊼{\phi }\right)⊼\left({\psi }⊼{\psi }\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 dfbi3 ${⊢}\left({\phi }↔{\psi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left(¬{\phi }\wedge ¬{\psi }\right)\right)$
2 df-or ${⊢}\left(\left({\phi }\wedge {\psi }\right)\vee \left(¬{\phi }\wedge ¬{\psi }\right)\right)↔\left(¬\left({\phi }\wedge {\psi }\right)\to \left(¬{\phi }\wedge ¬{\psi }\right)\right)$
3 df-nan ${⊢}\left({\phi }⊼{\psi }\right)↔¬\left({\phi }\wedge {\psi }\right)$
4 3 bicomi ${⊢}¬\left({\phi }\wedge {\psi }\right)↔\left({\phi }⊼{\psi }\right)$
5 nannot ${⊢}¬{\phi }↔\left({\phi }⊼{\phi }\right)$
6 nannot ${⊢}¬{\psi }↔\left({\psi }⊼{\psi }\right)$
7 5 6 anbi12i ${⊢}\left(¬{\phi }\wedge ¬{\psi }\right)↔\left(\left({\phi }⊼{\phi }\right)\wedge \left({\psi }⊼{\psi }\right)\right)$
8 4 7 imbi12i ${⊢}\left(¬\left({\phi }\wedge {\psi }\right)\to \left(¬{\phi }\wedge ¬{\psi }\right)\right)↔\left(\left({\phi }⊼{\psi }\right)\to \left(\left({\phi }⊼{\phi }\right)\wedge \left({\psi }⊼{\psi }\right)\right)\right)$
9 1 2 8 3bitri ${⊢}\left({\phi }↔{\psi }\right)↔\left(\left({\phi }⊼{\psi }\right)\to \left(\left({\phi }⊼{\phi }\right)\wedge \left({\psi }⊼{\psi }\right)\right)\right)$
10 nannan ${⊢}\left(\left({\phi }⊼{\psi }\right)⊼\left(\left({\phi }⊼{\phi }\right)⊼\left({\psi }⊼{\psi }\right)\right)\right)↔\left(\left({\phi }⊼{\psi }\right)\to \left(\left({\phi }⊼{\phi }\right)\wedge \left({\psi }⊼{\psi }\right)\right)\right)$
11 9 10 bitr4i ${⊢}\left({\phi }↔{\psi }\right)↔\left(\left({\phi }⊼{\psi }\right)⊼\left(\left({\phi }⊼{\phi }\right)⊼\left({\psi }⊼{\psi }\right)\right)\right)$