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

Theorem jctird 529
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 515 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  anc2ri  559  pm5.31  828  fnun  6435  fco  6503  mapdom2  8662  fisupg  8740  fiint  8769  dffi3  8869  fiinfg  8937  dfac2b  9530  cflm  9646  cfslbn  9663  cardmin  9960  fpwwe2lem12  10037  fpwwe2lem13  10038  elfznelfzob  13123  modsumfzodifsn  13292  dvdsdivcl  15642  isprm5  16025  latjlej1  17650  latmlem1  17666  cnrest2  21866  cnpresti  21868  trufil  22490  stdbdxmet  23097  lgsdir  25891  elwwlks2  27727  orthin  29204  mdbr2  30054  dmdbr2  30061  mdsl2i  30080  atcvat4i  30155  mdsymlem3  30163  wzel  33115  ontgval  33783  poimirlem3  34932  poimirlem4  34933  poimirlem29  34958  poimir  34962  cmtbr4N  36423  cvrat4  36611  cdlemblem  36961  negexpidd  39412  3cubeslem1  39414  ensucne0OLD  40027  itschlc0xyqsol  44937  elpglem2  44997
  Copyright terms: Public domain W3C validator