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

Theorem jctird 516
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 502 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  anc2ri  546  fnun  6137  fco  6198  mapdom2  8287  fisupg  8364  fiint  8393  dffi3  8493  fiinfg  8561  dfac2b  9153  dfac2OLD  9155  cflm  9274  cfslbn  9291  cardmin  9588  fpwwe2lem12  9665  fpwwe2lem13  9666  elfznelfzob  12782  modsumfzodifsn  12951  dvdsdivcl  15247  isprm5  15626  latjlej1  17273  latmlem1  17289  cnrest2  21311  cnpresti  21313  trufil  21934  stdbdxmet  22540  lgsdir  25278  elwwlks2  27115  orthin  28645  mdbr2  29495  dmdbr2  29502  mdsl2i  29521  atcvat4i  29596  mdsymlem3  29604  wzel  32106  ontgval  32767  poimirlem3  33745  poimirlem4  33746  poimirlem29  33771  poimir  33775  cmtbr4N  35064  cvrat4  35251  cdlemblem  35601  elpglem2  42986
  Copyright terms: Public domain W3C validator