# Metamath Proof Explorer

Description: An implication is equivalent to the equivalence of some implied equivalence and some other equivalence involving a conjunction. A utility lemma as illustrated in biadanii and elelb . (Contributed by BJ, 4-Mar-2023) (Proof shortened by Wolf Lammen, 8-Mar-2023)

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

### Proof

Step Hyp Ref Expression
1 pm4.71r ${⊢}\left({\phi }\to {\psi }\right)↔\left({\phi }↔\left({\psi }\wedge {\phi }\right)\right)$
2 bicom ${⊢}\left({\phi }↔\left({\psi }\wedge {\phi }\right)\right)↔\left(\left({\psi }\wedge {\phi }\right)↔{\phi }\right)$
3 bicom ${⊢}\left({\phi }↔\left({\psi }\wedge {\chi }\right)\right)↔\left(\left({\psi }\wedge {\chi }\right)↔{\phi }\right)$
4 pm5.32 ${⊢}\left({\psi }\to \left({\phi }↔{\chi }\right)\right)↔\left(\left({\psi }\wedge {\phi }\right)↔\left({\psi }\wedge {\chi }\right)\right)$
5 3 4 bibi12i ${⊢}\left(\left({\phi }↔\left({\psi }\wedge {\chi }\right)\right)↔\left({\psi }\to \left({\phi }↔{\chi }\right)\right)\right)↔\left(\left(\left({\psi }\wedge {\chi }\right)↔{\phi }\right)↔\left(\left({\psi }\wedge {\phi }\right)↔\left({\psi }\wedge {\chi }\right)\right)\right)$
6 bicom ${⊢}\left(\left({\psi }\to \left({\phi }↔{\chi }\right)\right)↔\left({\phi }↔\left({\psi }\wedge {\chi }\right)\right)\right)↔\left(\left({\phi }↔\left({\psi }\wedge {\chi }\right)\right)↔\left({\psi }\to \left({\phi }↔{\chi }\right)\right)\right)$
7 biluk ${⊢}\left(\left({\psi }\wedge {\phi }\right)↔{\phi }\right)↔\left(\left(\left({\psi }\wedge {\chi }\right)↔{\phi }\right)↔\left(\left({\psi }\wedge {\phi }\right)↔\left({\psi }\wedge {\chi }\right)\right)\right)$
8 5 6 7 3bitr4ri ${⊢}\left(\left({\psi }\wedge {\phi }\right)↔{\phi }\right)↔\left(\left({\psi }\to \left({\phi }↔{\chi }\right)\right)↔\left({\phi }↔\left({\psi }\wedge {\chi }\right)\right)\right)$
9 1 2 8 3bitri ${⊢}\left({\phi }\to {\psi }\right)↔\left(\left({\psi }\to \left({\phi }↔{\chi }\right)\right)↔\left({\phi }↔\left({\psi }\wedge {\chi }\right)\right)\right)$