Description: Virtual deduction proof of 3impexpbicomi . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.