Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  jctird 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
jctird.2
Assertion
Ref Expression
jctird

Proof of Theorem jctird
StepHypRef Expression
1 jctird.1 . 2
2 jctird.2 . . 3
32a1d 25 . 2
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369 This theorem is referenced by:  anc2ri  558  ifptru  1388  fnun  5692  fco  5746  mapdom2  7708  fisupg  7788  fiint  7817  dffi3  7911  dfac2  8532  cflm  8651  cfslbn  8668  cardmin  8960  fpwwe2lem12  9040  fpwwe2lem13  9041  elfznelfzob  11916  isprm5  14253  latjlej1  15695  latmlem1  15711  cnrest2  19787  cnpresti  19789  trufil  20411  stdbdxmet  21018  lgsdir  23605  usgraedg4  24387  wlkdvspth  24610  el2spthonot  24870  orthin  26364  mdbr2  27215  dmdbr2  27222  mdsl2i  27241  atcvat4i  27316  mdsymlem3  27324  wzel  29380  ontgval  29896  cmtbr4N  34980  cvrat4  35167  cdlemblem  35517 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