Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994) (Proof shortened by Wolf Lammen, 1-Nov-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ancld.1 | |- ( ph -> ( ps -> ch ) ) |
|
| Assertion | ancld | |- ( ph -> ( ps -> ( ps /\ ch ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ancld.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 2 | idd | |- ( ph -> ( ps -> ps ) ) |
|
| 3 | 2 1 | jcad | |- ( ph -> ( ps -> ( ps /\ ch ) ) ) |