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

Theorem jctird 565
 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 554 1 (𝜑 → (𝜓 → (𝜒𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  anc2ri  579  fnun  5911  fco  5971  mapdom2  8016  fisupg  8093  fiint  8122  dffi3  8220  fiinfg  8288  dfac2  8836  cflm  8955  cfslbn  8972  cardmin  9265  fpwwe2lem12  9342  fpwwe2lem13  9343  elfznelfzob  12440  modsumfzodifsn  12605  dvdsdivcl  14876  isprm5  15257  latjlej1  16888  latmlem1  16904  cnrest2  20900  cnpresti  20902  trufil  21524  stdbdxmet  22130  lgsdir  24857  usgraedg4  25916  wlkdvspth  26138  el2spthonot  26397  orthin  27689  mdbr2  28539  dmdbr2  28546  mdsl2i  28565  atcvat4i  28640  mdsymlem3  28648  wzel  31015  wzelOLD  31016  ontgval  31600  bj-xnex  32245  poimirlem3  32582  poimirlem4  32583  poimirlem29  32608  poimir  32612  cmtbr4N  33560  cvrat4  33747  cdlemblem  34097  elwwlks2  41170  elpglem2  42254
 Copyright terms: Public domain W3C validator