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

Theorem jctird 529
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 23 . 2  |-  ( ph  ->  ( ps  ->  th )
)
41, 3jcad 520 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  anc2ri  542  fnun  5551  fco  5600  abianfp  6716  mapdom2  7278  fisupg  7355  fiint  7383  dffi3  7436  dfac2  8011  cflm  8130  cfslbn  8147  cardmin  8439  fpwwe2lem12  8516  fpwwe2lem13  8517  elfznelfzob  11193  isprm5  13112  latjlej1  14494  latmlem1  14510  cnrest2  17350  cnpresti  17352  trufil  17942  stdbdxmet  18545  lgsdir  21114  usgraedg4  21406  wlkdvspth  21608  orthin  22948  mdbr2  23799  dmdbr2  23806  mdsl2i  23825  atcvat4i  23900  mdsymlem3  23908  soseq  25529  wzel  25575  ontgval  26181  2cshw1lem1  28248  el2spthonot  28337  cmtbr4N  30053  cvrat4  30240  cdlemblem  30590
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator