Implication elimination

  1. REDIRECT Modus ponens