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  6432  nnmord  6684  map0g  6856  mapsn  6858  enq0tr  7653  addnqprl  7748  addnqpru  7749  cauappcvgprlemdisj  7870  lttri3  8258  ltleap  8811  mulgt1  9042  nominpos  9381  uzind  9590  indstr  9826  eqreznegel  9847  ccatopth  11296  shftuz  11377  caucvgrelemcau  11540  sqrtsq  11604  mulcn2  11872  dvdsgcdb  12583  algcvgblem  12620  lcmdvdsb  12655  rpexp  12724  infpnlem1  12931  imasring  14076  unitmulclb  14127  cnntr  14948  cnrest2  14959  txlm  15002  metrest  15229  uspgr2wlkeq  16215  bj-om  16532