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  1742  equsexd  1743  rexim  2591  rr19.28v  2904  sotricim  4359  sotritrieq  4361  ordsucss  4541  ordpwsucss  4604  peano5  4635  iss  4993  funssres  5301  ssimaex  5625  elpreima  5684  resflem  5729  tposfo2  6334  nnmord  6584  map0g  6756  mapsn  6758  enq0tr  7518  addnqprl  7613  addnqpru  7614  cauappcvgprlemdisj  7735  lttri3  8123  ltleap  8676  mulgt1  8907  nominpos  9246  uzind  9454  indstr  9684  eqreznegel  9705  shftuz  10999  caucvgrelemcau  11162  sqrtsq  11226  mulcn2  11494  dvdsgcdb  12205  algcvgblem  12242  lcmdvdsb  12277  rpexp  12346  infpnlem1  12553  imasring  13696  unitmulclb  13746  cnntr  14545  cnrest2  14556  txlm  14599  metrest  14826  bj-om  15667