MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jctird Structured version   Visualization version   GIF 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 (𝜑 → (𝜓𝜒))
jctird.2 (𝜑𝜃)
Assertion
Ref Expression
jctird (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem jctird
StepHypRef Expression
1 jctird.1 . 2 (𝜑 → (𝜓𝜒))
2 jctird.2 . . 3 (𝜑𝜃)
32a1d 25 . 2 (𝜑 → (𝜓𝜃))
41, 3jcad 514 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  anc2ri  558  pm5.31  830  fnun  6619  fcof  6696  fcoOLD  6698  mapdom2  9099  fisupg  9242  fiint  9275  dffi3  9374  fiinfg  9442  dfac2b  10073  nnadju  10140  cflm  10193  cfslbn  10210  cardmin  10507  fpwwe2lem11  10584  fpwwe2lem12  10585  elfznelfzob  13685  modsumfzodifsn  13856  dvdsdivcl  16205  isprm5  16590  latjlej1  18349  latmlem1  18365  cnrest2  22653  cnpresti  22655  trufil  23277  stdbdxmet  23887  lgsdir  26696  elwwlks2  28953  orthin  30430  mdbr2  31280  dmdbr2  31287  mdsl2i  31306  atcvat4i  31381  mdsymlem3  31389  wzel  34438  ontgval  34932  poimirlem3  36110  poimirlem4  36111  poimirlem29  36136  poimir  36140  cmtbr4N  37746  cvrat4  37935  cdlemblem  38285  negexpidd  41034  3cubeslem1  41036  ensucne0OLD  41876  itschlc0xyqsol  46927  elpglem2  47231
  Copyright terms: Public domain W3C validator