Metamath Proof Explorer

Theorem ibi

Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003)

Ref Expression
Hypothesis ibi.1 φ φ ψ
Assertion ibi φ ψ


Step Hyp Ref Expression
1 ibi.1 φ φ ψ
2 id φ φ
3 2 1 mpbid φ ψ