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 ( ( 𝜑𝜒 ) ↔ ( 𝜓𝜒 ) )