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  4470  sotritrieq  4472  ordsucss  4653  ordpwsucss  4716  peano5  4747  iss  5112  funssres  5423  ssimaex  5767  elpreima  5831  resflem  5875  tposfo2  6543  nnmord  6795  map0g  6974  mapsn  6978  enq0tr  7807  addnqprl  7902  addnqpru  7903  cauappcvgprlemdisj  8024  lttri3  8411  ltleap  8968  mulgt1  9201  nominpos  9554  uzind  9767  indstr  10008  eqreznegel  10029  ccatopth  11509  shftuz  11603  caucvgrelemcau  11767  sqrtsq  11831  mulcn2  12102  dvdsgcdb  12814  algcvgblem  12851  lcmdvdsb  12886  rpexp  12956  infpnlem1  13166  imasring  14477  unitmulclb  14529  assapropd  15122  cnntr  15468  cnrest2  15479  txlm  15522  metrest  15749  bposlem7  16334  uspgr2wlkeq  16828  bj-om  17185