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 | ⊢ 𝜓 | |
| Assertion | jctl | ⊢ ( 𝜑 → ( 𝜓 ∧ 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | jctl.1 | ⊢ 𝜓 | |
| 2 | id | ⊢ ( 𝜑 → 𝜑 ) | |
| 3 | 2 1 | jctil | ⊢ ( 𝜑 → ( 𝜓 ∧ 𝜑 ) ) |