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 φ ψ φ
Assertion ibir φ ψ


Step Hyp Ref Expression
1 ibir.1 φ ψ φ
2 1 bicomd φ φ ψ
3 2 ibi φ ψ