Theorem jcad 305

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 138	. 2 |- ( ch -> ( th -> ( ch /\ th ) ) )
4	1, 2, 3	syl6c 66	1 |- ( ph -> ( ps -> ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  jca2  306  jctild  314  jctird  315  ancld  323  ancrd  324  anim12ii  341  equsex  1721  equsexd  1722  rexim  2564  rr19.28v  2870  sotricim  4308  sotritrieq  4310  ordsucss  4488  ordpwsucss  4551  peano5  4582  iss  4937  funssres  5240  ssimaex  5557  elpreima  5615  resflem  5660  tposfo2  6246  nnmord  6496  map0g  6666  mapsn  6668  enq0tr  7396  addnqprl  7491  addnqpru  7492  cauappcvgprlemdisj  7613  lttri3  7999  ltleap  8551  mulgt1  8779  nominpos  9115  uzind  9323  indstr  9552  eqreznegel  9573  shftuz  10781  caucvgrelemcau  10944  sqrtsq  11008  mulcn2  11275  dvdsgcdb  11968  algcvgblem  12003  lcmdvdsb  12038  rpexp  12107  infpnlem1  12311  cnntr  13019  cnrest2  13030  txlm  13073  metrest  13300  bj-om  13972