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

Theorem jctird 547
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 27 . 2  |-  ( ph  ->  ( ps  ->  th )
)
41, 3jcad 536 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  anc2ri  561  fnun  5698  fco  5754  mapdom2  7747  fisupg  7823  fiint  7852  dffi3  7949  fiinfg  8019  dfac2  8563  cflm  8682  cfslbn  8699  cardmin  8991  fpwwe2lem12  9068  fpwwe2lem13  9069  elfznelfzob  12016  isprm5  14644  latjlej1  16304  latmlem1  16320  cnrest2  20294  cnpresti  20296  trufil  20917  stdbdxmet  21522  lgsdir  24250  usgraedg4  25106  wlkdvspth  25330  el2spthonot  25590  orthin  27091  mdbr2  27941  dmdbr2  27948  mdsl2i  27967  atcvat4i  28042  mdsymlem3  28050  wzel  30508  ontgval  31090  poimirlem3  31863  poimirlem4  31864  poimirlem29  31889  poimir  31893  cmtbr4N  32746  cvrat4  32933  cdlemblem  33283
  Copyright terms: Public domain W3C validator