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

Theorem jctird 525
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 511 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 395
This theorem is referenced by:  anc2ri  555  pm5.31  829  fnun  6669  fcof  6746  fcoOLD  6748  mapdom2  9173  fisupg  9316  fiint  9350  dffi3  9456  fiinfg  9524  dfac2b  10155  nnadju  10222  cflm  10275  cfslbn  10292  cardmin  10589  fpwwe2lem11  10666  fpwwe2lem12  10667  elfznelfzob  13774  modsumfzodifsn  13945  dvdsdivcl  16296  isprm5  16681  latjlej1  18448  latmlem1  18464  cnrest2  23234  cnpresti  23236  trufil  23858  stdbdxmet  24468  lgsdir  27310  elwwlks2  29849  orthin  31328  mdbr2  32178  dmdbr2  32185  mdsl2i  32204  atcvat4i  32279  mdsymlem3  32287  wzel  35551  ontgval  36046  poimirlem3  37227  poimirlem4  37228  poimirlem29  37253  poimir  37257  cmtbr4N  38857  cvrat4  39046  cdlemblem  39396  negexpidd  42244  3cubeslem1  42246  tfsconcatb0  42915  ensucne0OLD  43102  gricer  47376  itschlc0xyqsol  48026  elpglem2  48329
  Copyright terms: Public domain W3C validator