Description: Biconditional form of e2 . syl6ib is e2bi without virtual deductions. (Contributed by Alan Sare, 10-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).
|- ( ch <-> th )
|- (. ph ,. ps ->. th ).
|- ( ch -> th )