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

Theorem jccir 541
Description: Inference conjoining a consequent of a consequent to the right of the consequent in an implication. See also ex-natded5.3i 25745. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by AV, 20-Aug-2019.)
Hypotheses
Ref Expression
jccir.1  |-  ( ph  ->  ps )
jccir.2  |-  ( ps 
->  ch )
Assertion
Ref Expression
jccir  |-  ( ph  ->  ( ps  /\  ch ) )

Proof of Theorem jccir
StepHypRef Expression
1 jccir.1 . 2  |-  ( ph  ->  ps )
2 jccir.2 . . 3  |-  ( ps 
->  ch )
31, 2syl 17 . 2  |-  ( ph  ->  ch )
41, 3jca 534 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  jccil  542  oelim2  7295  hashf1rn  12521  trclfv  13032  maxprmfct  14612  telgsums  17564  chpmat1dlem  19796  chpdmatlem2  19800  leordtvallem1  20163  leordtvallem2  20164  mbfmax  22512  wlklniswwlkn2  25314  relowlpssretop  31542  stoweidlem34  37512  smonoord  38165
  Copyright terms: Public domain W3C validator