MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jctird 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  5492  fco  5541  abianfp  6653  mapdom2  7215  fisupg  7292  fiint  7320  dffi3  7372  dfac2  7945  cflm  8064  cfslbn  8081  cardmin  8373  fpwwe2lem12  8450  fpwwe2lem13  8451  elfznelfzob  11121  isprm5  13040  latjlej1  14422  latmlem1  14438  cnrest2  17273  cnpresti  17275  trufil  17864  stdbdxmet  18436  lgsdir  20982  usgraedg4  21273  wlkdvspth  21457  orthin  22797  mdbr2  23648  dmdbr2  23655  mdsl2i  23674  atcvat4i  23749  mdsymlem3  23757  soseq  25279  ontgval  25896  cmtbr4N  29371  cvrat4  29558  cdlemblem  29908
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