Description: Implication form of sbcbii . sbcbi is sbcbiVD without virtual
deductions and was automatically derived from sbcbiVD using the tools
program translate..without..overwriting.cmd and Metamath's minimize
command. (Contributed by Alan Sare, 18-Mar-2012)(Proof modification is discouraged.)(New usage is discouraged.)