Description: Right biconditional form of e2 . syl6ibr is e2bir without virtual deductions. (Contributed by Alan Sare, 29-Apr-2011) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).
|- ( th <-> ch )
|- (. ph ,. ps ->. th ).
|- ( ch -> th )