Description: Virtual deduction proof of idiALT . 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.
|- ph
|- ( ph -> ph )