Metamath Proof Explorer


Theorem bibi2i

Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993) (Proof shortened by Andrew Salmon, 7-May-2011) (Proof shortened by Wolf Lammen, 16-May-2013)

Ref Expression
Hypothesis bibi2i.1
|- ( ph <-> ps )
Assertion bibi2i
|- ( ( ch <-> ph ) <-> ( ch <-> ps ) )

Proof

Step Hyp Ref Expression
1 bibi2i.1
 |-  ( ph <-> ps )
2 id
 |-  ( ( ch <-> ph ) -> ( ch <-> ph ) )
3 2 1 bitrdi
 |-  ( ( ch <-> ph ) -> ( ch <-> ps ) )
4 id
 |-  ( ( ch <-> ps ) -> ( ch <-> ps ) )
5 4 1 bitr4di
 |-  ( ( ch <-> ps ) -> ( ch <-> ph ) )
6 3 5 impbii
 |-  ( ( ch <-> ph ) <-> ( ch <-> ps ) )