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

Theorem jctird 544
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 25 . 2  |-  ( ph  ->  ( ps  ->  th )
)
41, 3jcad 533 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  anc2ri  558  fnun  5687  fco  5741  mapdom2  7689  fisupg  7769  fiint  7798  dffi3  7892  dfac2  8512  cflm  8631  cfslbn  8648  cardmin  8940  fpwwe2lem12  9020  fpwwe2lem13  9021  elfznelfzob  11885  isprm5  14115  latjlej1  15555  latmlem1  15571  cnrest2  19593  cnpresti  19595  trufil  20238  stdbdxmet  20845  lgsdir  23430  usgraedg4  24160  wlkdvspth  24383  el2spthonot  24643  orthin  26137  mdbr2  26988  dmdbr2  26995  mdsl2i  27014  atcvat4i  27089  mdsymlem3  27097  soseq  29187  wzel  29233  ontgval  29749  bj-iftru  33450  cmtbr4N  34269  cvrat4  34456  cdlemblem  34806
  Copyright terms: Public domain W3C validator