Description: Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021) (Proof shortened by Wolf Lammen, 26-Mar-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | simpl2im.1 | |- ( ph -> ( ps /\ ch ) ) |
|
| simpl2im.2 | |- ( ch -> th ) |
||
| Assertion | simpl2im | |- ( ph -> th ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl2im.1 | |- ( ph -> ( ps /\ ch ) ) |
|
| 2 | simpl2im.2 | |- ( ch -> th ) |
|
| 3 | 1 | simprd | |- ( ph -> ch ) |
| 4 | 3 2 | syl | |- ( ph -> th ) |