Theorem jccir 560

Description: Inference conjoining a consequent of a consequent to the right of the consequent in an implication. See also ex-natded5.3i 26658. (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 553	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  jccil  561  oelim2  7562  hashf1rnOLD  13005  trclfv  13589  maxprmfct  15259  telgsums  18213  chpmat1dlem  20459  chpdmatlem2  20463  leordtvallem1  20824  leordtvallem2  20825  mbfmax  23222  wlklniswwlkn2  26228  relowlpssretop  32388  ntrclsk13  37389  stoweidlem34  38927  smonoord  39944  1wlklnwwlkln2lem  41079  0wlkOnlem1  41286