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  1780  equsexd  1782  rexim  2644  rr19.28v  2966  sotricim  4463  sotritrieq  4465  ordsucss  4646  ordpwsucss  4709  peano5  4740  iss  5104  funssres  5415  ssimaex  5758  elpreima  5819  resflem  5863  tposfo2  6528  nnmord  6780  map0g  6959  mapsn  6962  enq0tr  7791  addnqprl  7886  addnqpru  7887  cauappcvgprlemdisj  8008  lttri3  8395  ltleap  8950  mulgt1  9183  nominpos  9522  uzind  9736  indstr  9972  eqreznegel  9993  ccatopth  11466  shftuz  11560  caucvgrelemcau  11724  sqrtsq  11788  mulcn2  12056  dvdsgcdb  12768  algcvgblem  12805  lcmdvdsb  12840  rpexp  12909  infpnlem1  13116  imasring  14342  unitmulclb  14394  cnntr  15249  cnrest2  15260  txlm  15303  metrest  15530  uspgr2wlkeq  16520  bj-om  16877