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  1751  equsexd  1752  rexim  2600  rr19.28v  2913  sotricim  4370  sotritrieq  4372  ordsucss  4552  ordpwsucss  4615  peano5  4646  iss  5005  funssres  5313  ssimaex  5640  elpreima  5699  resflem  5744  tposfo2  6353  nnmord  6603  map0g  6775  mapsn  6777  enq0tr  7547  addnqprl  7642  addnqpru  7643  cauappcvgprlemdisj  7764  lttri3  8152  ltleap  8705  mulgt1  8936  nominpos  9275  uzind  9484  indstr  9714  eqreznegel  9735  shftuz  11128  caucvgrelemcau  11291  sqrtsq  11355  mulcn2  11623  dvdsgcdb  12334  algcvgblem  12371  lcmdvdsb  12406  rpexp  12475  infpnlem1  12682  imasring  13826  unitmulclb  13876  cnntr  14697  cnrest2  14708  txlm  14751  metrest  14978  bj-om  15873