Theorem jccil

Description: Inference conjoining a consequent of a consequent to the left of the consequent in an implication. Remark: One can also prove this theorem using syl and jca (as done in jccir ), which would be 4 bytes shorter, but one step longer than the current proof. (Proof modification is discouraged.) (Contributed by AV, 20-Aug-2019)

	Ref	Expression
Hypotheses	jccir.1	|- ( ph -> ps )
	jccir.2	|- ( ps -> ch )
Assertion	jccil	|- ( ph -> ( ch /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		jccir.1	|- ( ph -> ps )
2		jccir.2	|- ( ps -> ch )
3	1 2	jccir	|- ( ph -> ( ps /\ ch ) )
4	3	ancomd	|- ( ph -> ( ch /\ ps ) )