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 ) ) )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  jca2  308  jctild  316  jctird  317  ancld  325  ancrd  326  anim12ii  343  equsex  1776  equsexd  1777  rexim  2626  rr19.28v  2946  sotricim  4420  sotritrieq  4422  ordsucss  4602  ordpwsucss  4665  peano5  4696  iss  5059  funssres  5369  ssimaex  5707  elpreima  5766  resflem  5811  tposfo2  6433  nnmord  6685  map0g  6857  mapsn  6859  enq0tr  7654  addnqprl  7749  addnqpru  7750  cauappcvgprlemdisj  7871  lttri3  8259  ltleap  8812  mulgt1  9043  nominpos  9382  uzind  9591  indstr  9827  eqreznegel  9848  ccatopth  11301  shftuz  11395  caucvgrelemcau  11558  sqrtsq  11622  mulcn2  11890  dvdsgcdb  12602  algcvgblem  12639  lcmdvdsb  12674  rpexp  12743  infpnlem1  12950  imasring  14096  unitmulclb  14147  cnntr  14968  cnrest2  14979  txlm  15022  metrest  15249  uspgr2wlkeq  16235  bj-om  16583