Description: Inference conjoining a theorem to the left of a consequent. (Contributed by NM, 31-Dec-1993) (Proof shortened by Wolf Lammen, 24-Oct-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | jctl.1 | |- ps |
|
| Assertion | jctl | |- ( ph -> ( ps /\ ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | jctl.1 | |- ps |
|
| 2 | id | |- ( ph -> ph ) |
|
| 3 | 2 1 | jctil | |- ( ph -> ( ps /\ ph ) ) |