Metamath Proof Explorer

Theorem ibir

Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004)

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

Proof

Step Hyp Ref Expression
1 ibir.1 
 |-  ( ph -> ( ps <-> ph ) )
2 1 bicomd 
 |-  ( ph -> ( ph <-> ps ) )
3 2 ibi 
 |-  ( ph -> ps )