Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  jccir Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 jccir.1 . 2 (𝜑𝜓)
2 jccir.2 . . 3 (𝜓𝜒)
31, 2syl 17 . 2 (𝜑𝜒)
41, 3jca 507 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator