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

Theorem jctird 526
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 512 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  anc2ri  556  pm5.31  831  fnun  6682  fcof  6759  brinxper  8774  mapdom2  9188  fisupg  9324  fiint  9366  fiintOLD  9367  dffi3  9471  fiinfg  9539  dfac2b  10171  nnadju  10238  cflm  10290  cfslbn  10307  cardmin  10604  fpwwe2lem11  10681  fpwwe2lem12  10682  elfznelfzob  13812  modsumfzodifsn  13985  dvdsdivcl  16353  isprm5  16744  latjlej1  18498  latmlem1  18514  cnrest2  23294  cnpresti  23296  trufil  23918  stdbdxmet  24528  lgsdir  27376  elwwlks2  29986  orthin  31465  mdbr2  32315  dmdbr2  32322  mdsl2i  32341  atcvat4i  32416  mdsymlem3  32424  wzel  35825  ontgval  36432  poimirlem3  37630  poimirlem4  37631  poimirlem29  37656  poimir  37660  cmtbr4N  39256  cvrat4  39445  cdlemblem  39795  negexpidd  42693  3cubeslem1  42695  tfsconcatb0  43357  ensucne0OLD  43543  itschlc0xyqsol  48688  elpglem2  49231
  Copyright terms: Public domain W3C validator