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  2943  sotricim  4414  sotritrieq  4416  ordsucss  4596  ordpwsucss  4659  peano5  4690  iss  5051  funssres  5360  ssimaex  5697  elpreima  5756  resflem  5801  tposfo2  6419  nnmord  6671  map0g  6843  mapsn  6845  enq0tr  7632  addnqprl  7727  addnqpru  7728  cauappcvgprlemdisj  7849  lttri3  8237  ltleap  8790  mulgt1  9021  nominpos  9360  uzind  9569  indstr  9800  eqreznegel  9821  ccatopth  11263  shftuz  11343  caucvgrelemcau  11506  sqrtsq  11570  mulcn2  11838  dvdsgcdb  12549  algcvgblem  12586  lcmdvdsb  12621  rpexp  12690  infpnlem1  12897  imasring  14042  unitmulclb  14093  cnntr  14914  cnrest2  14925  txlm  14968  metrest  15195  uspgr2wlkeq  16106  bj-om  16355