Theorem jctird 602

Description: Deduction conjoining a theorem to right of consequent in an implication.

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 12	. 2 |- (ph -> (ps -> th))
4	1, 3	jcad 600	1 |- (ph -> (ps -> (ch /\ th)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  fnun 3594  abianfp 3962  sdomdomtr 4469  fiint 4559  fiintOLD 4560  aceq6b 4742  cardmin 4860  cflim 4909  suplem1pr 5161  add20 5602  clim2serzt 7134  infxpidmlem8 7559  cnsscnp 7772  shlej1t 9355  orthin 9370  mdbr2 10223  dmdbr2 10230  mdsl2 10249  atcvat4 10324  mdsymlem3 10332

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain