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

Theorem jctird 544
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 533 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  anc2ri  558  fnun  5529  fco  5580  mapdom2  7494  fisupg  7572  fiint  7600  dffi3  7693  dfac2  8312  cflm  8431  cfslbn  8448  cardmin  8740  fpwwe2lem12  8820  fpwwe2lem13  8821  elfznelfzob  11643  isprm5  13810  latjlej1  15247  latmlem1  15263  cnrest2  18902  cnpresti  18904  trufil  19495  stdbdxmet  20102  lgsdir  22681  usgraedg4  23317  wlkdvspth  23519  orthin  24861  mdbr2  25712  dmdbr2  25719  mdsl2i  25738  atcvat4i  25813  mdsymlem3  25821  soseq  27727  wzel  27773  ontgval  28289  el2spthonot  30401  bj-iftru  32101  cmtbr4N  32912  cvrat4  33099  cdlemblem  33449
  Copyright terms: Public domain W3C validator