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