Metamath Proof Explorer
Theorem ibi
Description: Inference that converts a biconditional implied by one of its arguments,
into an implication. (Contributed by NM, 17Oct2003)


Ref 
Expression 

Hypothesis 
ibi.1 
$${\u22a2}{\phi}\to \left({\phi}\leftrightarrow {\psi}\right)$$ 

Assertion 
ibi 
$${\u22a2}{\phi}\to {\psi}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

ibi.1 
$${\u22a2}{\phi}\to \left({\phi}\leftrightarrow {\psi}\right)$$ 
2 

id 
$${\u22a2}{\phi}\to {\phi}$$ 
3 
2 1

mpbid 
$${\u22a2}{\phi}\to {\psi}$$ 