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	$$⊢\phi \to \psi$$
	jccir.2	$$⊢\psi \to \chi$$
Assertion	jccil	$$⊢\phi \to \left(\chi \wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		jccir.1	$$⊢\phi \to \psi$$
2		jccir.2	$$⊢\psi \to \chi$$
3	1 2	jccir	$$⊢\phi \to \left(\psi \wedge \chi \right)$$
4	3	ancomd	$$⊢\phi \to \left(\chi \wedge \psi \right)$$