# Metamath Proof Explorer

## Theorem pm4.71

Description: Implication in terms of biconditional and conjunction. Theorem *4.71 of WhiteheadRussell p. 120. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 2-Dec-2012)

Ref Expression
Assertion pm4.71 ${⊢}\left({\phi }\to {\psi }\right)↔\left({\phi }↔\left({\phi }\wedge {\psi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({\phi }\wedge {\psi }\right)\to {\phi }$
2 1 biantru ${⊢}\left({\phi }\to \left({\phi }\wedge {\psi }\right)\right)↔\left(\left({\phi }\to \left({\phi }\wedge {\psi }\right)\right)\wedge \left(\left({\phi }\wedge {\psi }\right)\to {\phi }\right)\right)$
3 anclb ${⊢}\left({\phi }\to {\psi }\right)↔\left({\phi }\to \left({\phi }\wedge {\psi }\right)\right)$
4 dfbi2 ${⊢}\left({\phi }↔\left({\phi }\wedge {\psi }\right)\right)↔\left(\left({\phi }\to \left({\phi }\wedge {\psi }\right)\right)\wedge \left(\left({\phi }\wedge {\psi }\right)\to {\phi }\right)\right)$
5 2 3 4 3bitr4i ${⊢}\left({\phi }\to {\psi }\right)↔\left({\phi }↔\left({\phi }\wedge {\psi }\right)\right)$