Theorem jcad 307

Description: Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)

Hypotheses

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

Assertion

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

Proof of Theorem jcad

Step	Hyp	Ref	Expression
1		jcad.1	. 2 |- ( ph -> ( ps -> ch ) )
2		jcad.2	. 2 |- ( ph -> ( ps -> th ) )
3		pm3.2 139	. 2 |- ( ch -> ( th -> ( ch /\ th ) ) )
4	1, 2, 3	syl6c 66	1 |- ( ph -> ( ps -> ( ch /\ th ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  jca2  308  jctild  316  jctird  317  ancld  325  ancrd  326  anim12ii  343  equsex  1780  equsexd  1782  rexim  2644  rr19.28v  2966  sotricim  4470  sotritrieq  4472  ordsucss  4653  ordpwsucss  4716  peano5  4747  iss  5112  funssres  5423  ssimaex  5767  elpreima  5831  resflem  5875  tposfo2  6542  nnmord  6794  map0g  6973  mapsn  6976  enq0tr  7807  addnqprl  7902  addnqpru  7903  cauappcvgprlemdisj  8024  lttri3  8411  ltleap  8968  mulgt1  9201  nominpos  9554  uzind  9768  indstr  10009  eqreznegel  10030  ccatopth  11510  shftuz  11604  caucvgrelemcau  11768  sqrtsq  11832  mulcn2  12103  dvdsgcdb  12815  algcvgblem  12852  lcmdvdsb  12887  rpexp  12957  infpnlem1  13167  imasring  14478  unitmulclb  14530  assapropd  15123  cnntr  15451  cnrest2  15462  txlm  15505  metrest  15732  bposlem7  16317  uspgr2wlkeq  16811  bj-om  17168