Theorem jccir 517

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

Hypotheses

Ref	Expression
jccir.1	⊢ (𝜑 → 𝜓)
jccir.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
jccir	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Proof of Theorem jccir

Step	Hyp	Ref	Expression
1		jccir.1	. 2 ⊢ (𝜑 → 𝜓)
2		jccir.2	. . 3 ⊢ (𝜓 → 𝜒)
3	1, 2	syl 17	. 2 ⊢ (𝜑 → 𝜒)
4	1, 3	jca 507	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199  df-an 387

This theorem is referenced by:  jccil  518  oelim2  7942  trclfv  14118  maxprmfct  15792  telgsums  18744  chpmat1dlem  21010  chpdmatlem2  21014  leordtvallem1  21385  leordtvallem2  21386  mbfmax  23815  wlklnwwlkln2lem  27182  0wlkonlem1  27483  relowlpssretop  33750  ntrclsk13  39202  stoweidlem34  41038  smonoord  42222