Theorem jcad 291

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 126	. 2 |- ( ch -> ( th -> ( ch /\ th ) ) )
4	1, 2, 3	syl6c 60	1 |- ( ph -> ( ps -> ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101

This theorem is referenced by:  jctild  299  jctird  300  ancld  308  ancrd  309  anim12ii  325  equsex  1616  equsexd  1617  rexim  2413  rr19.28v  2683  sotricim  4060  sotritrieq  4062  ordsucss  4230  ordpwsucss  4291  peano5  4321  iss  4654  funssres  4942  ssimaex  5234  elpreima  5286  tposfo2  5882  nnmord  6090  enq0tr  6532  addnqprl  6627  addnqpru  6628  cauappcvgprlemdisj  6749  lttri3  7098  ltleap  7621  mulgt1  7829  nominpos  8162  uzind  8349  indstr  8536  eqreznegel  8549  shftuz  9418  caucvgrelemcau  9579  sqrtsq  9642  mulcn2  9833  algcvgblem  9888  bj-om  10061  peano5setOLD  10065