Theorem jctird 567

Description: Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

Ref	Expression
jctird.1	|- ( ph -> ( ps -> ch ) )
jctird.2	|- ( ph -> th )

Assertion

Ref	Expression
jctird	|- ( ph -> ( ps -> ( ch /\ th ) ) )

Proof of Theorem jctird

Step	Hyp	Ref	Expression
1		jctird.1	. 2 |- ( ph -> ( ps -> ch ) )
2		jctird.2	. . 3 |- ( ph -> th )
3	2	a1d 25	. 2 |- ( ph -> ( ps -> th ) )
4	1, 3	jcad 555	1 |- ( ph -> ( ps -> ( ch /\ th ) ) )

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  581  fnun  5997  fco  6058  mapdom2  8131  fisupg  8208  fiint  8237  dffi3  8337  fiinfg  8405  dfac2  8953  cflm  9072  cfslbn  9089  cardmin  9386  fpwwe2lem12  9463  fpwwe2lem13  9464  elfznelfzob  12574  modsumfzodifsn  12743  dvdsdivcl  15038  isprm5  15419  latjlej1  17065  latmlem1  17081  cnrest2  21090  cnpresti  21092  trufil  21714  stdbdxmet  22320  lgsdir  25057  elwwlks2  26861  orthin  28305  mdbr2  29155  dmdbr2  29162  mdsl2i  29181  atcvat4i  29256  mdsymlem3  29264  wzel  31771  wzelOLD  31772  ontgval  32430  poimirlem3  33412  poimirlem4  33413  poimirlem29  33438  poimir  33442  cmtbr4N  34542  cvrat4  34729  cdlemblem  35079  elpglem2  42455