Theorem jctr

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

Proof

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