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  5350  fco  5398  abianfp  6471  mapdom2  7032  fisupg  7105  fiint  7133  dffi3  7184  dfac2  7757  cflm  7876  cfslbn  7893  cardmin  8186  fpwwe2lem12  8263  fpwwe2lem13  8264  isprm5  12791  latjlej1  14171  latmlem1  14187  cnrest2  17014  cnpresti  17016  trufil  17605  stdbdxmet  18061  lgsdir  20569  orthin  22025  mdbr2  22876  dmdbr2  22883  mdsl2i  22902  atcvat4i  22977  mdsymlem3  22985  issiga  23472  soseq  24254  ontgval  24870  cmtbr4N  29445  cvrat4  29632  cdlemblem  29982
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