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  7801  addnqprl  7896  addnqpru  7897  cauappcvgprlemdisj  8018  lttri3  8405  ltleap  8960  mulgt1  9193  nominpos  9543  uzind  9757  indstr  9993  eqreznegel  10014  ccatopth  11488  shftuz  11582  caucvgrelemcau  11746  sqrtsq  11810  mulcn2  12078  dvdsgcdb  12790  algcvgblem  12827  lcmdvdsb  12862  rpexp  12931  infpnlem1  13138  imasring  14369  unitmulclb  14421  assapropd  15014  cnntr  15326  cnrest2  15337  txlm  15380  metrest  15607  uspgr2wlkeq  16606  bj-om  16963