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  1750  equsexd  1751  rexim  2599  rr19.28v  2912  sotricim  4369  sotritrieq  4371  ordsucss  4551  ordpwsucss  4614  peano5  4645  iss  5004  funssres  5312  ssimaex  5639  elpreima  5698  resflem  5743  tposfo2  6352  nnmord  6602  map0g  6774  mapsn  6776  enq0tr  7546  addnqprl  7641  addnqpru  7642  cauappcvgprlemdisj  7763  lttri3  8151  ltleap  8704  mulgt1  8935  nominpos  9274  uzind  9483  indstr  9713  eqreznegel  9734  shftuz  11099  caucvgrelemcau  11262  sqrtsq  11326  mulcn2  11594  dvdsgcdb  12305  algcvgblem  12342  lcmdvdsb  12377  rpexp  12446  infpnlem1  12653  imasring  13797  unitmulclb  13847  cnntr  14668  cnrest2  14679  txlm  14722  metrest  14949  bj-om  15835