# Metamath Proof Explorer

## Theorem imnand2

Description: An -> nand relation. (Contributed by Anthony Hart, 2-Sep-2011)

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

### Proof

Step Hyp Ref Expression
1 nannot ${⊢}¬{\phi }↔\left({\phi }⊼{\phi }\right)$
2 nannot ${⊢}¬{\psi }↔\left({\psi }⊼{\psi }\right)$
3 1 2 anbi12i ${⊢}\left(¬{\phi }\wedge ¬{\psi }\right)↔\left(\left({\phi }⊼{\phi }\right)\wedge \left({\psi }⊼{\psi }\right)\right)$
4 3 notbii ${⊢}¬\left(¬{\phi }\wedge ¬{\psi }\right)↔¬\left(\left({\phi }⊼{\phi }\right)\wedge \left({\psi }⊼{\psi }\right)\right)$
5 iman ${⊢}\left(¬{\phi }\to {\psi }\right)↔¬\left(¬{\phi }\wedge ¬{\psi }\right)$
6 df-nan ${⊢}\left(\left({\phi }⊼{\phi }\right)⊼\left({\psi }⊼{\psi }\right)\right)↔¬\left(\left({\phi }⊼{\phi }\right)\wedge \left({\psi }⊼{\psi }\right)\right)$
7 4 5 6 3bitr4i ${⊢}\left(¬{\phi }\to {\psi }\right)↔\left(\left({\phi }⊼{\phi }\right)⊼\left({\psi }⊼{\psi }\right)\right)$