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  1739  equsexd  1740  rexim  2588  rr19.28v  2900  sotricim  4354  sotritrieq  4356  ordsucss  4536  ordpwsucss  4599  peano5  4630  iss  4988  funssres  5296  ssimaex  5618  elpreima  5677  resflem  5722  tposfo2  6320  nnmord  6570  map0g  6742  mapsn  6744  enq0tr  7494  addnqprl  7589  addnqpru  7590  cauappcvgprlemdisj  7711  lttri3  8099  ltleap  8651  mulgt1  8882  nominpos  9220  uzind  9428  indstr  9658  eqreznegel  9679  shftuz  10961  caucvgrelemcau  11124  sqrtsq  11188  mulcn2  11455  dvdsgcdb  12150  algcvgblem  12187  lcmdvdsb  12222  rpexp  12291  infpnlem1  12497  imasring  13560  unitmulclb  13610  cnntr  14393  cnrest2  14404  txlm  14447  metrest  14674  bj-om  15429