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

Theorem jctird 566
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 555 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  anc2ri  580  fnun  5955  fco  6015  mapdom2  8075  fisupg  8152  fiint  8181  dffi3  8281  fiinfg  8349  dfac2  8897  cflm  9016  cfslbn  9033  cardmin  9330  fpwwe2lem12  9407  fpwwe2lem13  9408  elfznelfzob  12515  modsumfzodifsn  12683  dvdsdivcl  14962  isprm5  15343  latjlej1  16986  latmlem1  17002  cnrest2  21000  cnpresti  21002  trufil  21624  stdbdxmet  22230  lgsdir  24957  elwwlks2  26728  orthin  28151  mdbr2  29001  dmdbr2  29008  mdsl2i  29027  atcvat4i  29102  mdsymlem3  29110  wzel  31469  wzelOLD  31470  ontgval  32069  bj-xnex  32698  poimirlem3  33041  poimirlem4  33042  poimirlem29  33067  poimir  33071  cmtbr4N  34019  cvrat4  34206  cdlemblem  34556  elpglem2  41745
  Copyright terms: Public domain W3C validator