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

Theorem jccir 561
Description: Inference conjoining a consequent of a consequent to the right of the consequent in an implication. See also ex-natded5.3i 27120. (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 554 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
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  562  oelim2  7620  hashf1rnOLD  13083  trclfv  13675  maxprmfct  15345  telgsums  18311  chpmat1dlem  20559  chpdmatlem2  20563  leordtvallem1  20924  leordtvallem2  20925  mbfmax  23322  wlklnwwlkln2lem  26637  0wlkonlem1  26845  relowlpssretop  32841  ntrclsk13  37848  stoweidlem34  39555  smonoord  40636
  Copyright terms: Public domain W3C validator