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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  jca2  308  jctild  316  jctird  317  ancld  325  ancrd  326  anim12ii  343  equsex  1780  equsexd  1782  rexim  2644  rr19.28v  2966  sotricim  4468  sotritrieq  4470  ordsucss  4651  ordpwsucss  4714  peano5  4745  iss  5109  funssres  5420  ssimaex  5764  elpreima  5828  resflem  5872  tposfo2  6538  nnmord  6790  map0g  6969  mapsn  6972  enq0tr  7802  addnqprl  7897  addnqpru  7898  cauappcvgprlemdisj  8019  lttri3  8406  ltleap  8963  mulgt1  9196  nominpos  9548  uzind  9762  indstr  10003  eqreznegel  10024  ccatopth  11504  shftuz  11598  caucvgrelemcau  11762  sqrtsq  11826  mulcn2  12097  dvdsgcdb  12809  algcvgblem  12846  lcmdvdsb  12881  rpexp  12951  infpnlem1  13161  imasring  14453  unitmulclb  14505  assapropd  15098  cnntr  15417  cnrest2  15428  txlm  15471  metrest  15698  bposlem7  16278  uspgr2wlkeq  16772  bj-om  17129