| [[apply-tactic\|apply]] *hypothesis* | Assuming an implication, convert a goal from a conclusion to a premise. | | ------------------------------------ | ----------------------------------------------------------------------- | If `hPimpQ : P → Q`is a hypotheses, and the goal is its conclusion type, `⊢ Q`, then invoking `apply hPimpQ` changes the goal from the conclusion to the premise type, `⊢ P`. Once the premise, `P` has been proven, it follows by `Modus Ponens (MP)`that the conclusion, `Q` is proven. ## Examples ### Proof of → Elim, (Modus Ponens) **`Video:`** #TODO **`GitHub:`** #TODO ### Proof of ∧ - Elim **`Video:`** #TODO **`GitHub:`** #TODO --- **`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date:`** 2026-08-11