Metamath Proof Explorer

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 ψ
Assertion jctr φ φ ψ


Step Hyp Ref Expression
1 jctl.1 ψ
2 id φ φ
3 2 1 jctir φ φ ψ