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

Theorem jctird 527
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 513 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  anc2ri  557  pm5.31  826  fnun  6456  fco  6524  mapdom2  8676  fisupg  8754  fiint  8783  dffi3  8883  fiinfg  8951  dfac2b  9544  cflm  9660  cfslbn  9677  cardmin  9974  fpwwe2lem12  10051  fpwwe2lem13  10052  elfznelfzob  13131  modsumfzodifsn  13300  dvdsdivcl  15654  isprm5  16039  latjlej1  17663  latmlem1  17679  cnrest2  21822  cnpresti  21824  trufil  22446  stdbdxmet  23052  lgsdir  25835  elwwlks2  27672  orthin  29150  mdbr2  30000  dmdbr2  30007  mdsl2i  30026  atcvat4i  30101  mdsymlem3  30109  wzel  33008  ontgval  33676  poimirlem3  34776  poimirlem4  34777  poimirlem29  34802  poimir  34806  cmtbr4N  36271  cvrat4  36459  cdlemblem  36809  negexpidd  39157  3cubeslem1  39159  ensucne0OLD  39774  itschlc0xyqsol  44682  elpglem2  44742
  Copyright terms: Public domain W3C validator