Description: Deduction eliminating a conjunct. (Contributed by NM, 14-May-1993) A translation of natural deduction rule /\ ER ( /\ elimination right), see natded . (Proof shortened by Wolf Lammen, 3-Oct-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | simprd.1 | |- ( ph -> ( ps /\ ch ) ) |
|
| Assertion | simprd | |- ( ph -> ch ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simprd.1 | |- ( ph -> ( ps /\ ch ) ) |
|
| 2 | 1 | ancomd | |- ( ph -> ( ch /\ ps ) ) |
| 3 | 2 | simpld | |- ( ph -> ch ) |