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  2944  sotricim  4418  sotritrieq  4420  ordsucss  4600  ordpwsucss  4663  peano5  4694  iss  5057  funssres  5366  ssimaex  5703  elpreima  5762  resflem  5807  tposfo2  6428  nnmord  6680  map0g  6852  mapsn  6854  enq0tr  7644  addnqprl  7739  addnqpru  7740  cauappcvgprlemdisj  7861  lttri3  8249  ltleap  8802  mulgt1  9033  nominpos  9372  uzind  9581  indstr  9817  eqreznegel  9838  ccatopth  11287  shftuz  11368  caucvgrelemcau  11531  sqrtsq  11595  mulcn2  11863  dvdsgcdb  12574  algcvgblem  12611  lcmdvdsb  12646  rpexp  12715  infpnlem1  12922  imasring  14067  unitmulclb  14118  cnntr  14939  cnrest2  14950  txlm  14993  metrest  15220  uspgr2wlkeq  16162  bj-om  16468