Metamath Proof Explorer
Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3May1994) (Proof shortened by Wolf Lammen, 22Sep2013)


Ref 
Expression 

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

Assertion 
biimpcd 
$${\u22a2}{\psi}\to \left({\phi}\to {\chi}\right)$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

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

syl5ibcom 
$${\u22a2}{\psi}\to \left({\phi}\to {\chi}\right)$$ 