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

Theorem jctird 542
Description: Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
Hypotheses
Ref Expression
jctird.1  |-  ( ph  ->  ( ps  ->  ch ) )
jctird.2  |-  ( ph  ->  th )
Assertion
Ref Expression
jctird  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )

Proof of Theorem jctird
StepHypRef Expression
1 jctird.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 jctird.2 . . 3  |-  ( ph  ->  th )
32a1d 25 . 2  |-  ( ph  ->  ( ps  ->  th )
)
41, 3jcad 531 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  anc2ri  556  ifptru  1391  fnun  5669  fco  5723  mapdom2  7681  fisupg  7760  fiint  7789  dffi3  7883  dfac2  8502  cflm  8621  cfslbn  8638  cardmin  8930  fpwwe2lem12  9008  fpwwe2lem13  9009  elfznelfzob  11897  isprm5  14337  latjlej1  15894  latmlem1  15910  cnrest2  19954  cnpresti  19956  trufil  20577  stdbdxmet  21184  lgsdir  23803  usgraedg4  24589  wlkdvspth  24812  el2spthonot  25072  orthin  26562  mdbr2  27413  dmdbr2  27420  mdsl2i  27439  atcvat4i  27514  mdsymlem3  27522  wzel  29620  ontgval  30124  cmtbr4N  35377  cvrat4  35564  cdlemblem  35914
  Copyright terms: Public domain W3C validator