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

Theorem jctird 568
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 556 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 197  df-an 385
This theorem is referenced by:  anc2ri  582  fnun  6158  fco  6219  mapdom2  8296  fisupg  8373  fiint  8402  dffi3  8502  fiinfg  8570  dfac2b  9143  dfac2OLD  9145  cflm  9264  cfslbn  9281  cardmin  9578  fpwwe2lem12  9655  fpwwe2lem13  9656  elfznelfzob  12768  modsumfzodifsn  12937  dvdsdivcl  15240  isprm5  15621  latjlej1  17266  latmlem1  17282  cnrest2  21292  cnpresti  21294  trufil  21915  stdbdxmet  22521  lgsdir  25256  elwwlks2  27088  orthin  28614  mdbr2  29464  dmdbr2  29471  mdsl2i  29490  atcvat4i  29565  mdsymlem3  29573  wzel  32075  ontgval  32736  poimirlem3  33725  poimirlem4  33726  poimirlem29  33751  poimir  33755  cmtbr4N  35045  cvrat4  35232  cdlemblem  35582  elpglem2  42968
  Copyright terms: Public domain W3C validator