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  1739  equsexd  1740  rexim  2588  rr19.28v  2901  sotricim  4355  sotritrieq  4357  ordsucss  4537  ordpwsucss  4600  peano5  4631  iss  4989  funssres  5297  ssimaex  5619  elpreima  5678  resflem  5723  tposfo2  6322  nnmord  6572  map0g  6744  mapsn  6746  enq0tr  7496  addnqprl  7591  addnqpru  7592  cauappcvgprlemdisj  7713  lttri3  8101  ltleap  8653  mulgt1  8884  nominpos  9223  uzind  9431  indstr  9661  eqreznegel  9682  shftuz  10964  caucvgrelemcau  11127  sqrtsq  11191  mulcn2  11458  dvdsgcdb  12153  algcvgblem  12190  lcmdvdsb  12225  rpexp  12294  infpnlem1  12500  imasring  13563  unitmulclb  13613  cnntr  14404  cnrest2  14415  txlm  14458  metrest  14685  bj-om  15499