Metamath Proof Explorer

Theorem jccir

Description: Inference conjoining a consequent of a consequent to the right of the consequent in an implication. See also ex-natded5.3i . (Contributed by Mario Carneiro, 9-Feb-2017) (Revised by AV, 20-Aug-2019)

Ref Expression
Hypotheses jccir.1 φ ψ
jccir.2 ψ χ
Assertion jccir φ ψ χ


Step Hyp Ref Expression
1 jccir.1 φ ψ
2 jccir.2 ψ χ
3 1 2 syl φ χ
4 1 3 jca φ ψ χ