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  1776  equsexd  1778  rexim  2636  rr19.28v  2957  sotricim  4444  sotritrieq  4446  ordsucss  4626  ordpwsucss  4689  peano5  4720  iss  5084  funssres  5395  ssimaex  5738  elpreima  5797  resflem  5841  tposfo2  6498  nnmord  6750  map0g  6922  mapsn  6925  enq0tr  7749  addnqprl  7844  addnqpru  7845  cauappcvgprlemdisj  7966  lttri3  8353  ltleap  8906  mulgt1  9137  nominpos  9476  uzind  9689  indstr  9925  eqreznegel  9946  ccatopth  11408  shftuz  11502  caucvgrelemcau  11665  sqrtsq  11729  mulcn2  11997  dvdsgcdb  12709  algcvgblem  12746  lcmdvdsb  12781  rpexp  12850  infpnlem1  13057  imasring  14208  unitmulclb  14259  cnntr  15090  cnrest2  15101  txlm  15144  metrest  15371  uspgr2wlkeq  16360  bj-om  16707