Description: Inference conjoining a theorem to the right of a consequent. (Contributed by NM, 18-Aug-1993) (Proof shortened by Wolf Lammen, 24-Oct-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | jctl.1 | ⊢ 𝜓 | |
| Assertion | jctr | ⊢ ( 𝜑 → ( 𝜑 ∧ 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | jctl.1 | ⊢ 𝜓 | |
| 2 | id | ⊢ ( 𝜑 → 𝜑 ) | |
| 3 | 2 1 | jctir | ⊢ ( 𝜑 → ( 𝜑 ∧ 𝜓 ) ) |