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

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