Theorem jcad 305

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 138	. 2 |- ( ch -> ( th -> ( ch /\ th ) ) )
4	1, 2, 3	syl6c 66	1 |- ( ph -> ( ps -> ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  jca2  306  jctild  314  jctird  315  ancld  323  ancrd  324  anim12ii  341  equsex  1716  equsexd  1717  rexim  2560  rr19.28v  2866  sotricim  4301  sotritrieq  4303  ordsucss  4481  ordpwsucss  4544  peano5  4575  iss  4930  funssres  5230  ssimaex  5547  elpreima  5604  resflem  5649  tposfo2  6235  nnmord  6485  map0g  6654  mapsn  6656  enq0tr  7375  addnqprl  7470  addnqpru  7471  cauappcvgprlemdisj  7592  lttri3  7978  ltleap  8530  mulgt1  8758  nominpos  9094  uzind  9302  indstr  9531  eqreznegel  9552  shftuz  10759  caucvgrelemcau  10922  sqrtsq  10986  mulcn2  11253  dvdsgcdb  11946  algcvgblem  11981  lcmdvdsb  12016  rpexp  12085  infpnlem1  12289  cnntr  12875  cnrest2  12886  txlm  12929  metrest  13156  bj-om  13829