# Metamath Proof Explorer

## Theorem df3an2

Description: Express triple-and in terms of implication and negation. Statement in Frege1879 p. 12. (Contributed by RP, 25-Jul-2020)

Ref Expression
Assertion df3an2 ${⊢}\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔¬\left({\phi }\to \left({\psi }\to ¬{\chi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 df-3an ${⊢}\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\wedge {\chi }\right)$
2 df-an ${⊢}\left(\left({\phi }\wedge {\psi }\right)\wedge {\chi }\right)↔¬\left(\left({\phi }\wedge {\psi }\right)\to ¬{\chi }\right)$
3 impexp ${⊢}\left(\left({\phi }\wedge {\psi }\right)\to ¬{\chi }\right)↔\left({\phi }\to \left({\psi }\to ¬{\chi }\right)\right)$
4 2 3 xchbinx ${⊢}\left(\left({\phi }\wedge {\psi }\right)\wedge {\chi }\right)↔¬\left({\phi }\to \left({\psi }\to ¬{\chi }\right)\right)$
5 1 4 bitri ${⊢}\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔¬\left({\phi }\to \left({\psi }\to ¬{\chi }\right)\right)$