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  1752  equsexd  1753  rexim  2601  rr19.28v  2917  sotricim  4378  sotritrieq  4380  ordsucss  4560  ordpwsucss  4623  peano5  4654  iss  5014  funssres  5322  ssimaex  5653  elpreima  5712  resflem  5757  tposfo2  6366  nnmord  6616  map0g  6788  mapsn  6790  enq0tr  7567  addnqprl  7662  addnqpru  7663  cauappcvgprlemdisj  7784  lttri3  8172  ltleap  8725  mulgt1  8956  nominpos  9295  uzind  9504  indstr  9734  eqreznegel  9755  ccatopth  11192  shftuz  11203  caucvgrelemcau  11366  sqrtsq  11430  mulcn2  11698  dvdsgcdb  12409  algcvgblem  12446  lcmdvdsb  12481  rpexp  12550  infpnlem1  12757  imasring  13901  unitmulclb  13951  cnntr  14772  cnrest2  14783  txlm  14826  metrest  15053  bj-om  16011