Description: Deduction joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Proof shortened by Wolf Lammen, 10-Apr-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | jcnd.1 | |- ( ph -> ps ) |
|
| jcnd.2 | |- ( ph -> -. ch ) |
||
| Assertion | jcnd | |- ( ph -> -. ( ps -> ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | jcnd.1 | |- ( ph -> ps ) |
|
| 2 | jcnd.2 | |- ( ph -> -. ch ) |
|
| 3 | jcn | |- ( ps -> ( -. ch -> -. ( ps -> ch ) ) ) |
|
| 4 | 1 2 3 | sylc | |- ( ph -> -. ( ps -> ch ) ) |