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

Theorem jctird 528
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 22 . 2  |-  ( ph  ->  ( ps  ->  th )
)
41, 3jcad 519 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  anc2ri  541  fnun  5366  fco  5414  abianfp  6487  mapdom2  7048  fisupg  7121  fiint  7149  dffi3  7200  dfac2  7773  cflm  7892  cfslbn  7909  cardmin  8202  fpwwe2lem12  8279  fpwwe2lem13  8280  isprm5  12807  latjlej1  14187  latmlem1  14203  cnrest2  17030  cnpresti  17032  trufil  17621  stdbdxmet  18077  lgsdir  20585  orthin  22041  mdbr2  22892  dmdbr2  22899  mdsl2i  22918  atcvat4i  22993  mdsymlem3  23001  issiga  23487  soseq  24325  ontgval  24942  wlkdvspth  28366  cmtbr4N  30067  cvrat4  30254  cdlemblem  30604
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 177  df-an 360
  Copyright terms: Public domain W3C validator