Theorem jctl

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	$$⊢\psi$$
Assertion	jctl	$$⊢\phi \to \left(\psi \wedge \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		jctl.1	$$⊢\psi$$
2		id	$$⊢\phi \to \phi$$
3	2 1	jctil	$$⊢\phi \to \left(\psi \wedge \phi \right)$$