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  2627  rr19.28v  2947  sotricim  4426  sotritrieq  4428  ordsucss  4608  ordpwsucss  4671  peano5  4702  iss  5065  funssres  5376  ssimaex  5716  elpreima  5775  resflem  5819  tposfo2  6476  nnmord  6728  map0g  6900  mapsn  6902  enq0tr  7697  addnqprl  7792  addnqpru  7793  cauappcvgprlemdisj  7914  lttri3  8301  ltleap  8854  mulgt1  9085  nominpos  9424  uzind  9635  indstr  9871  eqreznegel  9892  ccatopth  11346  shftuz  11440  caucvgrelemcau  11603  sqrtsq  11667  mulcn2  11935  dvdsgcdb  12647  algcvgblem  12684  lcmdvdsb  12719  rpexp  12788  infpnlem1  12995  imasring  14141  unitmulclb  14192  cnntr  15019  cnrest2  15030  txlm  15073  metrest  15300  uspgr2wlkeq  16289  bj-om  16636