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  1774  equsexd  1775  rexim  2624  rr19.28v  2943  sotricim  4413  sotritrieq  4415  ordsucss  4595  ordpwsucss  4658  peano5  4689  iss  5050  funssres  5359  ssimaex  5694  elpreima  5753  resflem  5798  tposfo2  6411  nnmord  6661  map0g  6833  mapsn  6835  enq0tr  7617  addnqprl  7712  addnqpru  7713  cauappcvgprlemdisj  7834  lttri3  8222  ltleap  8775  mulgt1  9006  nominpos  9345  uzind  9554  indstr  9784  eqreznegel  9805  ccatopth  11243  shftuz  11323  caucvgrelemcau  11486  sqrtsq  11550  mulcn2  11818  dvdsgcdb  12529  algcvgblem  12566  lcmdvdsb  12601  rpexp  12670  infpnlem1  12877  imasring  14022  unitmulclb  14072  cnntr  14893  cnrest2  14904  txlm  14947  metrest  15174  bj-om  16258