Theorem jccir 562

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  jccil  563  oelim2  7675  hashf1rnOLD  13143  trclfv  13741  maxprmfct  15421  telgsums  18390  chpmat1dlem  20640  chpdmatlem2  20644  leordtvallem1  21014  leordtvallem2  21015  mbfmax  23416  wlklnwwlkln2lem  26768  0wlkonlem1  26979  relowlpssretop  33212  ntrclsk13  38369  stoweidlem34  40251  smonoord  41341