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	|- ps
Assertion	jctr	|- ( ph -> ( ph /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		jctl.1	|- ps
2		id	|- ( ph -> ph )
3	2 1	jctir	|- ( ph -> ( ph /\ ps ) )