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 φ ψ
Assertion bibi2i χ φ χ ψ

Proof

Step Hyp Ref Expression
1 bibi2i.1 φ ψ
2 id χ φ χ φ
3 2 1 bitrdi χ φ χ ψ
4 id χ ψ χ ψ
5 4 1 bitr4di χ ψ χ φ
6 3 5 impbii χ φ χ ψ