Metamath Proof Explorer


Theorem bibi1i

Description: Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993)

Ref Expression
Hypothesis bibi2i.1 φ ψ
Assertion bibi1i φ χ ψ χ

Proof

Step Hyp Ref Expression
1 bibi2i.1 φ ψ
2 bicom φ χ χ φ
3 1 bibi2i χ φ χ ψ
4 bicom χ ψ ψ χ
5 2 3 4 3bitri φ χ ψ χ