Description: Right biconditional form of e1a . sylibr is e1bir without virtual deductions. (Contributed by Alan Sare, 24-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).
|- ( ch <-> ps )
|- (. ph ->. ch ).
|- ( ps -> ch )