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  5510  fco  5559  abianfp  6675  mapdom2  7237  fisupg  7314  fiint  7342  dffi3  7394  dfac2  7967  cflm  8086  cfslbn  8103  cardmin  8395  fpwwe2lem12  8472  fpwwe2lem13  8473  elfznelfzob  11148  isprm5  13067  latjlej1  14449  latmlem1  14465  cnrest2  17304  cnpresti  17306  trufil  17895  stdbdxmet  18498  lgsdir  21067  usgraedg4  21359  wlkdvspth  21561  orthin  22901  mdbr2  23752  dmdbr2  23759  mdsl2i  23778  atcvat4i  23853  mdsymlem3  23861  soseq  25468  ontgval  26085  el2spthonot  28067  cmtbr4N  29738  cvrat4  29925  cdlemblem  30275
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