# Metamath Proof Explorer

## Theorem bibi2d

Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-1993) (Proof shortened by Wolf Lammen, 19-May-2013)

Ref Expression
Hypothesis imbid.1 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
Assertion bibi2d ${⊢}{\phi }\to \left(\left({\theta }↔{\psi }\right)↔\left({\theta }↔{\chi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 imbid.1 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
2 1 pm5.74i ${⊢}\left({\phi }\to {\psi }\right)↔\left({\phi }\to {\chi }\right)$
3 2 bibi2i ${⊢}\left(\left({\phi }\to {\theta }\right)↔\left({\phi }\to {\psi }\right)\right)↔\left(\left({\phi }\to {\theta }\right)↔\left({\phi }\to {\chi }\right)\right)$
4 pm5.74 ${⊢}\left({\phi }\to \left({\theta }↔{\psi }\right)\right)↔\left(\left({\phi }\to {\theta }\right)↔\left({\phi }\to {\psi }\right)\right)$
5 pm5.74 ${⊢}\left({\phi }\to \left({\theta }↔{\chi }\right)\right)↔\left(\left({\phi }\to {\theta }\right)↔\left({\phi }\to {\chi }\right)\right)$
6 3 4 5 3bitr4i ${⊢}\left({\phi }\to \left({\theta }↔{\psi }\right)\right)↔\left({\phi }\to \left({\theta }↔{\chi }\right)\right)$
7 6 pm5.74ri ${⊢}{\phi }\to \left(\left({\theta }↔{\psi }\right)↔\left({\theta }↔{\chi }\right)\right)$